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

• 作者: 缪淮扣 许庆国
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 实时系统 时间Büchi自动机 时间化时序逻辑 PVS
• 年，卷（期）: 2006,（12）
• 所属期刊栏目: 软件工程
• 页码范围: 238-242
• 页数: 5页
• 分类号: TP3
• 字数: 6016字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2006.12.064

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	缪淮扣	上海大学计算机学院	100	1030	16.0	26.0
2	许庆国	上海大学计算机学院	9	35	4.0	5.0