《實時安全關鍵系統的建模、仿真與驗證》是依託西安電子科技大學，由王小兵擔任項目負責人的面上項目。
基本介紹
- 中文名：實時安全關鍵系統的建模、仿真與驗證
- 項目類別：面上項目
- 項目負責人：王小兵
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
擴展投影時序邏輯PTL(Projection Temporal Logic)為實時時序邏輯TPTL(Timed PTL)，研究其語法、語義及邏輯規則。定義TPTL的命題子集-TPPTL(Timed Propositional PTL)作為實時安全關鍵系統(Real-Time Safety-Critical System,RTSCS)的規範語言，並研究其可判定性與判定算法。定義TPTL的可執行子集-實時時序邏輯程式設計語言RT-MSVL(Real-Time Modeling,Simulation and Verification Language)作為RTSCS的建模語言，研究其操作語義。研究RT-MSVL的解釋執行技術與模型檢測算法，設計並實現集建模、仿真與驗證於一體的RT-MSVL解釋器。將TPPTL與RT-MSVL套用於典型RTSCS，例如高速列車控制系統，研究其建模、仿真與驗證技術。
結題摘要
實時安全關鍵系統(Real-Time Safety-Critical System，RTSCS)要求在確定時間內完成系統功能，執行動作需要滿足特定的時間約束。為了減少或防止RTSCS發生災難性事故，研究了該類系統的關鍵科學問題，以期保證它們的安全性與正確性。在投影時序邏輯PTL(Projection Temporal Logic)的基礎上，建立了TPTL(Time PTL)系統，增加了量化的時間概念用於表達絕對時間約束，定義了導出公式用於表達相對時間約束以及其它RTSCS需要的重要時間約束。研究了TPTL的邏輯規則，基於範式與範式圖給出了在無窮模型下的高效判定算法。從TPTL中抽取一個可執行子集，在MSVL(Modeling, Simulation and Verification Language)的基礎上，建立了實時時序邏輯程式設計語言TMSVL(Timed MSVL)，包含了中斷、逾時以及延遲等實時描述語句。建立了基於TPTL與TMSVL的RTSCS驗證理論與方法：使用TMSVL程式對RTSCS進行建模，使用TPTL公式對期望性質進行描述，將模型與性質統一在TPTL的框架中。對原有的MSV(Modeling, Simulation and Verification)平台進行擴展，實現了TMSV(Timed MSV)平台，能夠接受TPTL公式與TMSVL程式，用於對RTSCS進行建模、仿真與驗證。使用該方法在TMSV平台中實現了典型RTSCS的建模、仿真與驗證：主要針對高速列車控制系統CTCS-3規範，使用TMSVL對各個子系統與場景進行建模，驗證了若干條實時關鍵性質。
