草稿:Uppaal模型检查器
 | 本草稿尚未提交审核
提交前，请先查阅维基百科不是什么，以免犯下常见错误。 要让草稿被接受，需要至少满足以下要求：
我们强烈不鼓励您创建与您自己、您所在的组织、其对手或其产品相关的条目。如果您仍要这么做，请申报利益冲突。 注意：若您提交之后，本模板出现在页面最下方，表示您已成功提交。
如何改善您的草稿
|  |
UPPAAL是一个用于对实时系统进行建模、确认和验证的集成工具环境，该系统以时序自动机网络为模型基础，并扩展到几种额外的数据类型（有界整数、数组等）。
自 1995 年发布以来，它已在至少 17 个研究案例中使用，包括Lego Mindstorms 、飞利浦音频协议和Mecel的变速箱控制器。 [1]
该工具是由瑞典乌普萨拉大学实时系统设计与分析小组和丹麦奥尔堡大学计算机科学基础研究中心合作开发的。
有以下可用的扩展：
- Cora用于成本最优可达性分析。
- Tron用于在线测试实时系统（黑盒一致性测试）。
- CoVer 最佳离线测试生成。
- Tiga用于基于时序游戏 (TImed GAmes) 的控制器合成。
- 基于组件的定时系统的 port，利用偏序缩减技术。
- Pro 用于概率可达性分析。 （已停止维护）
- SMC用于统计模型检查。