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