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

摘要

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