实时安全关键系统的建模、仿真与验证

基金项目类型：

国家自然科学基金

基金项目编号：

61272118

来源网站：

国家自然科学基金委员会

来源网址：

http://www.nsfc.gov.cn/

负责人：

王小兵

完成单位：

西安电子科技大学

中文关键词：

时序逻辑; 时序逻辑语言; 实时安全关键系统; 模型检测;

其他语种关键词：

temporal logic; temporal logic languages; real-time safety-critical system; model checking

项目类型：

面上项目

语种：

中文

开始日期：

2013-01-01

结束日期：

2016-12-31

中文摘要：

扩展投影时序逻辑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，例如高速列车控制系统，研究其建模、仿真与验证技术。