基于驗證的軟件架構演化分析與評估.pdf

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

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

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

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