基于驗(yàn)證的軟件架構(gòu)演化分析與評(píng)估.pdf

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

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

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

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