标签：#软件验证

Uppaal模型检查器

UPPAAL是一个用于对实时系统进行建模、确认和验证的集成工具环境，该系统以时序自动机网络为模型基础，并扩展到几种额外的数据类型（有界整数、数组等）。 自 1995 年发布以来，它已在至少 17 个研究案例中使用，包括Lego Mindstorms 、飞利浦音频协议和Mecel的变速箱控制器。 该工具是由瑞典乌普萨拉大学实时系统设计与分析小组和丹麦奥尔堡大学计算机科学基础研究中心合作开发的。 有以下可用的扩展： Cora用于成本最优可达…