基于時間自動機的實時系統建模及驗證
2011-01-01 00:00:00吳永剛陸慧娟程倬等
計算機時代 2011年6期
摘要：實時系統必須在一個事先定義好的時間限制內對來自外部或內部的事件進行響應，如何有效驗證實時模型的正確性和安全性是一個難點。文章通過多個時間自動機來模擬實時系統中的各個對象，并用uPPAAL對模型進行驗證，減少了模型驗證的狀態搜索空間，為實時嵌入式系統開發和驗證提供了一種可行、安全的控制機制。實驗結果顯示了系統的有效性。
關鍵詞：時間自動機；實時系統；UPPAAL；模型驗證
