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

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

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