基于时间自动机的模型验证软件 Uppaal是一个集成化的对实时系统建模、确认和验证的工具,它采用一组带有整型变量的时间自动机对实时系统的行为进行模拟和验证,采用的模型检查机制可以避免状态空间的爆炸,已被广泛的应用于算法分析和协议验证方面。Uppaal使用的是客户端-服务器的系统结构,分为图形界面和模型检测引擎。
uppaaltron在线测试实时系统的工具 Uppaal TRON 是一种基于Uppaal engine的在线测试工具, 它适用于对实时系统(主要是对实时嵌入式软件)的黑盒一致性测试,。本文介绍了Uppaal TRON的构成、特征以及优缺点,语法, 语义和语用, 列举了它的几种扩展形式, 并归纳了其应用及研究现状.