基于驗證的軟件架構(gòu)演化分析與評估.pdf

1、演化反映了“在演化實體或其組成元素的屬性方面不斷改進(jìn)的過程”，而軟件演化就是指軟件系統(tǒng)或內(nèi)部組成元素不斷地改變來滿足新的功能需求或?qū)傩孕枨?。在現(xiàn)代軟件系統(tǒng)的生命周期內(nèi)，演化是一項貫穿始終的活動，系統(tǒng)需求的改變、功能實現(xiàn)的增強(qiáng)、新型算法的發(fā)現(xiàn)、運行環(huán)境的改變等等均要求軟件系統(tǒng)具有較強(qiáng)的演化能力，這就要求能夠保障系統(tǒng)的正確性。而隨著軟件架構(gòu)的發(fā)展，作為軟件生命周期中的早期設(shè)計產(chǎn)品，架構(gòu)從全局和整體的角度為系統(tǒng)提供結(jié)構(gòu)、行為和屬性等信息，使得

2、架構(gòu)設(shè)計的演化結(jié)果的正確與否十分關(guān)鍵。
　　本文重點關(guān)注對于軟件架構(gòu)演化的分析，以及對架構(gòu)及架構(gòu)演化的正確性驗證。由于架構(gòu)設(shè)計的復(fù)雜化，使得對架構(gòu)正確與否的人工判斷工作變得復(fù)雜化和難以保證準(zhǔn)確性，而模型檢驗的方法能夠有效地驗證架構(gòu)演化的正確與否，來完成這項工作?；谀Ｐ蜋z驗的工具Spin能夠有效地實現(xiàn)對架構(gòu)設(shè)計的正確性驗證，但是其所需要的Promela模型無法進(jìn)行直觀的建模工作，不具有通用性，使得在此基礎(chǔ)上的演化工作難以進(jìn)行。因此

3、，這需要建立一個架構(gòu)模型來幫助驗證和演化分析工作。
　　本文使用UML(Unified Modeling Language)作為架構(gòu)描述的輸入，針對于架構(gòu)設(shè)計的正確性相關(guān)的UML順序圖，采用擴(kuò)展層次自動機(jī)對其進(jìn)行建模，作為驗證和演化分析的基礎(chǔ)。本文首先介紹了基于Spin的軟件架構(gòu)驗證方法，將架構(gòu)設(shè)計文檔轉(zhuǎn)換成擴(kuò)展層次自動機(jī)模型，采用線性時態(tài)邏輯語言LTL對架構(gòu)約束進(jìn)行描述，從自動機(jī)模型和LTL生成Promela模型，采用Spin進(jìn)

4、行驗證并獲得單版本的驗證結(jié)果。而后，論文描述了架構(gòu)演化的過程，并在層次自動機(jī)模型的基礎(chǔ)上詳細(xì)分析順序圖中的各種元素，包括對象、消息和復(fù)合片段，從它們的各自操作出發(fā)，分析各個元素的演化方式和演化規(guī)則。而后，在此基礎(chǔ)上提出了一個基于驗證的架構(gòu)演化分析和評估方法，從各個版本的驗證結(jié)果中可以獲取演化的信息，以及演化對架構(gòu)正確性產(chǎn)生的影響，從而完成對演化的分析與評估工作。最后論文通過Hadoop和MVC兩個實驗，分別說明了在不清楚演化過程和清楚演