论文部分内容阅读
实时嵌入式系统的重时间特性决定了在系统设计时需对系统作确定性验证。本文分析了不同的验证方法后认为形式化验证中基于时间自动机的模型检验方法最适用于实时嵌入式系统的分析和验证。在此基础上本文给出了时间自动机的定义和验证性工具UPPAAL的介绍,并对行人优先可控交通灯控制系统实例做了详细的建模、验证分析,结果表明该系统满足预定的各种特性要求。
The heavy-time nature of real-time embedded systems determines the need for system-specific verification of the system. After analyzing different verification methods, this paper considers that the time-automata-based model checking method in formal verification is most suitable for the analysis and verification of real-time embedded systems. On this basis, this paper gives an introduction of UPPAAL, a definition and verification tool of timed automaton, and gives a detailed modeling and verification analysis of pedestrian priority controllable traffic light control system. The results show that the system satisfies the predetermined Species requirements.