实时系统形式规格说明在PVS中的建立  

Formalizing Real-time Specification Using the Timed Temporal Logic in PVS

作　　者：许庆国[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机学院,上海200072

出　　处：《计算机科学》2006年第12期238-242,共5页Computer Science

基　　金：国家自然科学基金项目(批准号60173031);国家973项目(编号:2002CB312001)资助。

摘　　要：本文首先简介了时间自动机和时间B櫣chi自动机形式模型,结合时间化时序逻辑(TimedTemporalLogic)的语法和语义,利用定理证明器PVS(PrototypeVerificationSystem)实现了定义在时间自动机状态(或运行)上的时间化分支(或线性)时序逻辑规格说明的形式体系。在此基础上,结合一个经典的实时系统实例,用该体系对其实时特性进行了形式描述和形式验证,并得到了良好的结果。On the Basis of the formal model of the timed automata, timed Büchi automata and the formal syntax and semantics of the timed temporal logic, some formal theories about timed branch （linear） temporal logic are implemented over the states （runs） of the timed automata using PVS （Prototype Verification System） in this paper. A well-known real-time system model by timed automata and its real-time specifications are investigated using these theories. The results show the formal verification of real-time specification using the formalization in this paper is effective.

关 键 词：实时系统 时间Büchi自动机 时间化时序逻辑 PVS 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]