草稿:Uppaal 模型检查器
UPPAAL是一个用于对实时系统进行建模、确认和验证的集成工具环境，该系统以时序自动机网络为模型基础，并扩展到几种额外的数据类型（有界整数、数组等）。
自 1995 年发布以来，它已在至少 17 个研究案例中使用，包括Lego Mindstorms 、飞利浦音频协议和Mecel的变速箱控制器。 [1]
该工具是由瑞典乌普萨拉大学实时系统设计与分析小组和丹麦奥尔堡大学计算机科学基础研究中心合作开发的。
有以下可用的扩展：
- Cora用于成本最优可达性分析。
- Tron用于在线测试实时系统（黑盒一致性测试）。
- 涵盖COVERerage 最佳离线测试生成。
- Tiga用于基于时序游戏 (TImed GAmes) 的控制器合成。
- 基于组件的定时系统的端口，利用偏序缩减技术。
- Pro用于概率可达性分析。 （已停止维护）
- SMC用于统计模型检查。