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

项目名称： 实时安全关键系统的建模、仿真与验证

项目编号： No.61272118

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 王小兵

作者单位： 西安电子科技大学

项目金额： 80万元

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

中文关键词： 时序逻辑；时序逻辑语言；实时安全关键系统；模型检测；

英文摘要： The syntax,semantics and logic laws of Timed Projection Temporal Logic(TPTL) are investigated based on Projection Temporal Logic.Timed Propositional PTL(TPPTL) which is a propositional subset of TPTL is defined as a specification language for Real-Time Safety-Critical System(RTSCS), then its decidability and decision algorithm are studied.A real-time temporal logic programming language RT-MSVL(Real-Time Modeling, Simulation and Verification Languag)which is an executable subset of TPTL is formalized as an modeling language for RTSCS, and its operational semantics are explored. The interpreter of RT-MSVL is designed and developed according to its reduction rules and model checking algorithm, which is a uniform modeling, simulation and verification platform with real-time temporal logic for RTSCS.TPPTL and RT-MSVL are applied to model, simulate and verify RTSCS to ensure their safety and reliability, such as high-speed railway control systems.

英文关键词： temporal logic；temporal logic languages；real-time safety-critical system；model checking；