论文部分内容阅读
本文首先简介了时间自动机和时间Büchi自动机形式模型，结合时间化时序逻辑（Timed Temporal Logic）的语法和语义，利用定理证明器PVS（Prototype Verification System）实现了定义在时间自动机状态（或运行）上的时间化分支（或线性）时序逻辑规格说明的形式体系。在此基础上，结合一个经典的实时系统实例，用该体系对其实时特性进行了形式描述和形式验证，并得到了良好的结果。