基于扩展Petri网的系统建模及形式化验证方法

• 作者: 刘铭 姚爱红 张国印 门朝光
• 来源期刊: 计算机应用研究
• 关键词: 形式化验证 建模 实时有色Petri网 嵌入式系统
• 年，卷（期）: 2010,（12）
• 页码范围: 4587-4590
• 分类号: TP301
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2010.12.056

摘要

嵌入式实时系统对时间约束性、安全性和可靠性具有非常高的要求,但是传统的建模和形式化验证方法难以满足对系统的实时性和安全性的模拟和验证需求.通过对有色Petri网的时间属性进行扩展,提出了实时有色Petri网模型,能够对系统的时间属性进行模拟和评估;参考实时有色Petri网模型到时间自动机的语义转换规则对模型进行转换,可以利用时间计算树逻辑对系统的实时性、安全性和可靠性进行形式化验证.以列车通信网络控制器的双线冗余控制模块的建模和形式化验证为例,证明了该方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张国印	哈尔滨工程大学计算机科学与技术学院	162	1407	18.0	28.0
2	姚爱红	哈尔滨工程大学计算机科学与技术学院	25	173	9.0	11.0
3	刘铭	哈尔滨工程大学计算机科学与技术学院	19	155	8.0	12.0
4	门朝光	哈尔滨工程大学计算机科学与技术学院	52	319	11.0	15.0