基于擴展Pe州網(wǎng)的系統(tǒng)建模及形式化驗證方法
2010-12-31 00:00:00張國印劉銘姚愛紅門朝光
計算機應(yīng)用研究 2010年12期
摘 要：嵌入式實時系統(tǒng)對時間約束性、安全性和可靠性具有非常高的要求，但是傳統(tǒng)的建模和形式化驗證方法難以滿足對系統(tǒng)的實時性和安全性的模擬和驗證需求。通過對有色Petri網(wǎng)的時間屬性進行擴展，提出了實時有色Petri網(wǎng)模型，能夠?qū)ο到y(tǒng)的時間屬性進行模擬和評估；參考實時有色Petri網(wǎng)模型到時間自動機的語義轉(zhuǎn)換規(guī)則對模型進行轉(zhuǎn)換，可以利用時間計算樹邏輯對系統(tǒng)的實時性、安全性和可靠性進行形式化驗證。以列車通信網(wǎng)絡(luò)控制器的雙線冗余控制模塊的建模和形式化驗證為倒，證明了該方法的有效性。關(guān)鍵詞：形式化驗證；建模；實時有色Petri網(wǎng)；嵌入式系統(tǒng)
