实时嵌入式系统形式化自动验证的研究与应用

• 作者: 李迪 肖舒华 苏兆港 郑建华
• 来源期刊: 制造业自动化
• 学科: 工学
• 关键词: 实时嵌入式系统 UPPAAL 时间自动机 交通灯控制
• 年，卷（期）: 2007,（9）
• 所属期刊栏目: 研究与开发
• 页码范围: 20-24
• 页数: 5页
• 分类号: TP301.1
• 字数: 4999字
• 语种: 中文
• DOI: 10.3969/j.issn.1009-0134.2007.09.005

摘要

实时嵌入式系统的重时间特性决定了在系统设计时需对系统作确定性验证.本文分析了不同的验证方法后认为形式化验证中基于时间自动机的模型检验方法最适用于实时嵌入式系统的分析和验证.在此基础上本文给出了时间自动机的定义和验证性工具UPPAAL的介绍,并对行人优先可控交通灯控制系统实例做了详细的建模、验证分析,结果表明该系统满足预定的各种特性要求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李迪	华南理工大学机械工程学院	145	1331	20.0	27.0
2	郑建华	仲恺农业技术学院计算机科学与工程学院	34	99	5.0	8.0
3	肖舒华	华南理工大学机械工程学院	1	6	1.0	1.0
4	苏兆港	华南理工大学机械工程学院	2	8	2.0	2.0