实时系统的形式化验证

• 作者: 王戟 胡成军 陈火旺
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 实时系统 带时戳时序逻辑 形式验证
• 年，卷（期）: 2000,（2）
• 所属期刊栏目: 实时系统
• 页码范围: 46-48,53
• 页数: 4页
• 分类号: TP303
• 字数: 3109字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2000.02.015

摘要

实时系统的设计对系统设计人员而言是一个巨大挑战.在缺乏严格的验证环境时,要避免设计错误是很困难的.本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到HOL定理证明器中,并实现了一个基本的规则策略库,从而实现了一个简单的交互式辅助验证环境LRP.实例Fisher算法的互斥性在IRP中得到了验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王戟		41	880	14.0	29.0
2	胡成军		14	58	5.0	6.0
3	陈火旺		56	1155	18.0	33.0