系统建模与验证工具 - Uppaal

[houdini]

Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).

非常好的工具，声明与函数定义语法基本与C语言想同，查询语句为CTL语法，提供GUI和CLI两种界面，核心算法采用C++，支持Linux、windows、MacOS 等各种平台。


http://www.uppaal.com/

[_____]

状态机模型？

[eexpress]

作什么的？能吃饭不

[forrid]

谢，去look

[houdini]

作什么的？能吃饭不

模型验证。

举例： 电梯模型 至少应该满足以下下两个性质：

1. 如果有人在第n层按下了向上（或向下）箭头，那么最终他会得到服务;
2. 如果有人在第n层申请服务，那么电梯不应该在未响应此服务前经过(traverse)第n层。

用uppaal建模可以验证在你的模型里这些性质是否成立并追踪其状态迁移轨迹。 对大多数问题，由于计算量太大手工进行几乎不可能。

网上流传的4人打手电过桥问题也可用此工具建模并验证。

在网络协议里也有一些应用。

[stlxv]

作什么的？能吃饭不

模型验证。

举例： 电梯模型 至少应该满足以下下两个性质：

1. 如果有人在第n层按下了向上（或向下）箭头，那么最终他会得到服务;
2. 如果有人在第n层申请服务，那么电梯不应该在未响应此服务前经过(traverse)第n层。

用uppaal建模可以验证在你的模型里这些性质是否成立并追踪其状态迁移轨迹。 对大多数问题，由于计算量太大手工进行几乎不可能。

网上流传的4人打手电过桥问题也可用此工具建模并验证。

在网络协议里也有一些应用。

最终还是要通过数学方法来证明……

[kqueenc]

我们学校就用这个工具教学的。
因为……这个工具就是我们学校教研组开发的

[乖娃娃]

请问：UPPAAL可以在哪里下载？