（國防科學技術大學計算機學院 湖南 長沙 410073）
摘要：傳統的模型檢驗技術能夠表示出實時系統的性質和規范，但是實時系統的實時約束大多基于抽象層次的實時模型來描述，無法與具體的程序相關聯，難以體現系統的實際運行效果。本文以某航天程序為例，通過TCTL建立系統模型，在此基礎上引入WCET技術，將模型的狀態和實時約束對應到具體的程序片段上，分析了程序片段的最差情況執行時間并反饋到系統模型中。增強了模型的描述能力，為軟件系統的進一步升級和維護提供支持。
關鍵詞：模型檢驗；實時系統；TCTL；WCET；
參考文獻
[1] Manna Z.Pnueli A Models for reactivity 1993(07)
[2] 張廣泉 基于線性時序邏輯的實時系統建模與求精 小型微型計算機系統 2006年8月
[3] J.P. Queille, J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. M. Dezani-Ciancaglini, U. Montanari, (Editors) International Symposium on Programming. Springer-Verlag, 1982, vol. 137 of Lecture Notes in Computer Science, 216-230.
[5] Joost-Pieter Katoen,Concepts, Algorithms, and Tools For Model Checking 205~206
[6] PETER PUSCHNER and A.Burns. Guest Editorial: A Review of Worst-Case Execution-Time Analysis, Real-Tim Systems, May 2000, 18(2-3): 115~128
[7] The Programming Language wcetC. http://www.vmars.tuwien.ac.at/~raimund/calc_wcet/.18 July 2001.2~6
[8] PETER PUSCHNER and A.Burns. Guest Editorial: A Review of Worst-Case Execution-Time Analysis, Real-Tim Systems, May 2000, 18(2-3): 115~128.
作者簡介：
張曦（1983-），男，江蘇淮安人，國防科學技術大學計算機學院碩士二年級學生，主要研究方向為面向模型的可信性分析與驗證。
