一種演化超圖文法到狀態(tài)轉(zhuǎn)移系統(tǒng)的映射方法

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

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

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