| 实时嵌入式系统形式化自动验证的研究与应用 |
| |
| 引用本文： | 郑建华,李迪,肖舒华,苏兆港.实时嵌入式系统形式化自动验证的研究与应用[J].制造业自动化,2007,29(9):20-24. |
| |
| 作者姓名： | 郑建华 李迪 肖舒华 苏兆港 |
| |
| 作者单位： | 1. 仲恺农业技术学院计算机科学与工程学院,广州,510225
2. 华南理工大学机械工程学院,广州,510640 |
| |
| 基金项目： | 国家自然科学基金(50575075)，广东省科技计划资助项目(2002C1020407)资助 |
| |
| 摘 要： | 实时嵌入式系统的重时间特性决定了在系统设计时需对系统作确定性验证。本文分析了不同的验证方法后认为形式化验证中基于时间自动机的模型检验方法最适用于实时嵌入式系统的分析和验证。在此基础上本文给出了时间自动机的定义和验证性工具UPPAAL的介绍,并对行人优先可控交通灯控制系统实例做了详细的建模、验证分析,结果表明该系统满足预定的各种特性要求。
|
| 关 键 词： | 实时嵌入式系统 UPPAAL 时间自动机 交通灯控制 |
| 文章编号： | 1009-0134（2007）09-0020-04 |
| 修稿时间： | 2007-04-10 |
The research and application of formal auto-verification for real-time embedded system |
| |
| ZHENG Jian-hua,LI Di,XIAO Shu-hua,SHU Zhao-gang.The research and application of formal auto-verification for real-time embedded system[J].Manufacturing Automation,2007,29(9):20-24. |
| |
| Authors: | ZHENG Jian-hua LI Di XIAO Shu-hua SHU Zhao-gang |
| |
| Abstract: | It is necessary to finish the verification for real-time embedded system during the system design period because of the time constraint in the system.After analyzing severa methodologies,the paper concludes that model checking of formal verification based on Timed Automaton is a useful method to analyze and verify the real-time embedded system Then the paper gives the definitions of Timed Automation and the introduction of mode checkers tool UPPAAL.In the end the applicaton of a passenger priority traffic light contro system is described:including the detailed process of modeling and verification.The resul proves that the system meets the requirements. |
| |
| Keywords: | real-time embedded system UPPAAL Timed Automaton(TA) traffic light control |
| 本文献已被 维普 万方数据 等数据库收录！ |
