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

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.

扩展投影时序逻辑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对各个子系统与场景进行建模，验证了若干条实时关键性质。