隨著計算機技術和網(wǎng)絡技術的不斷發(fā)展，Internet已成為當今主流的軟件運行環(huán)境，在Internet開放環(huán)境下，軟件的用戶需求、計算環(huán)境等不斷發(fā)生改變，當面對這些變化的需求和環(huán)境時，軟件往往需要不斷動態(tài)演化才能增強生命力，才能適者生存．支持動態(tài)演化的軟件能在運行時改變系統(tǒng)的實現(xiàn)，包括完善系統(tǒng)功能、改變體系結構等，而無需重啟或重編譯系統(tǒng)．軟件演化己成為軟件生命周期中的重要組成部分，而軟件動態(tài)演化由于具有持續(xù)可用等優(yōu)點，則逐漸成為軟件工程領域研究的熱點．

　　軟件體系結構SA（software architecture）描述了軟件系統(tǒng)的結構組成、組成元素之問的交互、連接及約束等．由于在軟件設計中的核心地位，SA很自然地成為研究軟件動態(tài)演化的重要組成部分．SA動態(tài)演化是指SA的組成元素、拓撲結構、交互關系等在系統(tǒng)運行時被改變或調(diào)整的過程，這種行為也通常稱為SA運行時重配置（reconfiguration），很長一段時問以來，如何建模動態(tài)演化，是SA演化研究領域的主要焦點．然而，如何驗證動態(tài)演化的正確性，是近年來SA演化領域面臨的更大挑戰(zhàn)．因為即使運用形式化建模技術。也不能完全保證SA動態(tài)演化的正確性．為了保證演化的正確性，SA動態(tài)演化必須滿足一定的性質，且必須驗證這些性質得到滿足．模型檢測（model checking）作為近20年來最為流行的形式化驗證技術之一，已被逐漸運用于驗證SA動態(tài)演化的正確性．然而，當前這方面的研究很少考慮SA動態(tài)演化時的相關條件．

　　針對這一問題，本文在前期工作的基礎上，提出用條件狀態(tài)轉移系統(tǒng)表示SA動態(tài)演化的狀態(tài)模型，用抽象狀態(tài)機ASM（abstract state machine）作為SA動態(tài)演化條件超圖文法和條件狀態(tài)轉移系統(tǒng)的統(tǒng)一語義表示，將動態(tài)演化過程中的SA超圖映射為狀態(tài)，SA演化規(guī)則運用映射為條件狀態(tài)轉移關系，給出SA動態(tài)演化的條件超圖文法到條件狀態(tài)轉移系統(tǒng)的映射方法和實現(xiàn)算法，并證明了在該映射方法下，SA動態(tài)演化的條件超圖文法與條件狀態(tài)轉移系統(tǒng)的互模擬等價．最后，通過案例分析，運用本文的方法和模型檢測技術驗證了案例系統(tǒng)SA動態(tài)演化的相關性質，從而驗證了本文方法的有效性．