可重構(gòu)離散事件控制系統(tǒng)的建模與驗(yàn)證.pdf

1、現(xiàn)代技術(shù)系統(tǒng)大多依賴于復(fù)雜控制技術(shù)、計(jì)算機(jī)技術(shù)和網(wǎng)絡(luò)通信技術(shù)。由于各種信號(hào)并發(fā)、沖突等的存在，導(dǎo)致系統(tǒng)的動(dòng)態(tài)行為錯(cuò)綜復(fù)雜。因此，往往將這些系統(tǒng)抽象為離散事件控制系統(tǒng)來研究。動(dòng)態(tài)可重構(gòu)系統(tǒng)是未來復(fù)雜技術(shù)系統(tǒng)的趨勢(shì)，如安全關(guān)鍵的核電系統(tǒng)、飛控系統(tǒng)和普通的汽車電子系統(tǒng)、自動(dòng)化制造系統(tǒng)等。這種系統(tǒng)可以根據(jù)系統(tǒng)內(nèi)、外執(zhí)行環(huán)境的變化，如部分組件故障、網(wǎng)絡(luò)阻塞、未知干擾、用戶請(qǐng)求等，主動(dòng)地修改當(dāng)前構(gòu)型的部分組件、組件間連接關(guān)系和數(shù)據(jù)等，使當(dāng)前構(gòu)型在線

2、地轉(zhuǎn)變?yōu)榱硪环N構(gòu)型，從而保證系統(tǒng)能夠持續(xù)地滿足控制需求。基于模型的設(shè)計(jì)方法能夠較早發(fā)現(xiàn)復(fù)雜技術(shù)系統(tǒng)的設(shè)計(jì)缺陷、提高系統(tǒng)的可靠性、縮短開發(fā)系統(tǒng)所耗費(fèi)的時(shí)間，因此被廣泛地關(guān)注和應(yīng)用。一個(gè)準(zhǔn)確、簡(jiǎn)潔且易于分析的系統(tǒng)形式化模型是基于模型設(shè)計(jì)方法的第一步。在此基礎(chǔ)上采用形式化驗(yàn)證方法能夠全面測(cè)試被設(shè)計(jì)的系統(tǒng)是否滿足需求并為改進(jìn)系統(tǒng)設(shè)計(jì)方案提供可靠依據(jù)。本文研究的主要內(nèi)容就是可重構(gòu)離散事件控制系統(tǒng)的形式化建模與驗(yàn)證。
　　NCES是Petri

3、網(wǎng)的一種模塊化擴(kuò)展形式化體系。其清晰的模塊化結(jié)構(gòu)適合于建模可重構(gòu)離散事件控制系統(tǒng)。本文首先重點(diǎn)研究了三種基于NCES網(wǎng)的可能的重構(gòu)方案:第一種是對(duì)庫所的修改，第二種是對(duì)變遷的修改，第三種是對(duì)系統(tǒng)初始標(biāo)識(shí)的修改。相應(yīng)地，一種基于NCES的嵌套的狀態(tài)機(jī)被用來分別處理這三種重構(gòu)方案的控制實(shí)施。最終得到的系統(tǒng)模型的正確性由軟件SESA檢驗(yàn)，其中功能特性由計(jì)算樹邏輯及其擴(kuò)展邏輯描述。
　　考慮到直接用NCES或者TNCES建模可重構(gòu)控制系統(tǒng)

4、會(huì)給后續(xù)系統(tǒng)驗(yàn)證帶來較大負(fù)擔(dān)，本文提出了一種新的形式化體系R-TNCES。一個(gè)R-TNCES由一個(gè)控制模塊和一個(gè)行為模塊組成。其中，行為模塊由多個(gè)交疊的TNCES組成，控制模塊由一組重構(gòu)函數(shù)組成。這些重構(gòu)函數(shù)根據(jù)執(zhí)行環(huán)境的改變自動(dòng)地切換行為模塊中的TNCES。此外，考慮到R-TNCES中各個(gè)TNCES的相似性，一個(gè)分層驗(yàn)證的方法被提了出來，用以控制對(duì)R-TNCES驗(yàn)證的復(fù)雜性。
　　為了保證分布式可重構(gòu)離散事件控制系統(tǒng)的一致性，本

5、文提出了一種新的協(xié)調(diào)方法。系統(tǒng)中的每一個(gè)可重構(gòu)的分系統(tǒng)都由一個(gè)R-TNCES來表示。一個(gè)虛擬協(xié)調(diào)器和該協(xié)調(diào)器與各分系統(tǒng)間的通信協(xié)議被建立起來處理分系統(tǒng)間的一致性問題。這種方法可以達(dá)到兩個(gè)效果:1）給出最優(yōu)重構(gòu)方案，2）減少分系統(tǒng)間的通信量。此外，為了保證這種協(xié)調(diào)方法的正確性，采用了基于計(jì)算樹邏輯的模型檢驗(yàn)技術(shù)來驗(yàn)證整個(gè)系統(tǒng)的各種行為。
　　最后，為了有效分析動(dòng)態(tài)重構(gòu)過程中的系統(tǒng)行為，本文進(jìn)一步擴(kuò)展了R-TNCES。首先，在重構(gòu)函數(shù)