系统建模与验证工具 - Uppaal

仅仅用于软件推荐,不适合发求软件或软件使用问题方面的贴子
回复
头像
houdini
帖子: 250
注册时间: 2006-04-08 22:07
送出感谢: 0
接收感谢: 0
联系:

系统建模与验证工具 - Uppaal

#1

帖子 houdini » 2007-06-12 13:49

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/
附件
uppaal1.png
Modeling
uppaal2.png
Simulation
uppaal4.png
Verification
An Addicted KDE User
_____
帖子: 207
注册时间: 2007-05-21 11:30
送出感谢: 0
接收感谢: 0

#2

帖子 _____ » 2007-06-12 19:26

:shock: 状态机模型?
头像
eexpress
帖子: 58428
注册时间: 2005-08-14 21:55
来自: 长沙
送出感谢: 4 次
接收感谢: 256 次

#3

帖子 eexpress » 2007-06-12 19:27

作什么的?能吃饭不
● 鸣学
头像
forrid
帖子: 659
注册时间: 2007-04-23 17:40
送出感谢: 0
接收感谢: 0

#4

帖子 forrid » 2007-06-13 19:19

谢,去look

吾生也有涯,而知也无涯,以有涯随无涯,SB啊~~~~~~~~~~
头像
houdini
帖子: 250
注册时间: 2006-04-08 22:07
送出感谢: 0
接收感谢: 0
联系:

#5

帖子 houdini » 2007-06-15 12:36

eexpress 写了:作什么的?能吃饭不
模型验证。

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

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

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

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

在网络协议里也有一些应用。
An Addicted KDE User
头像
stlxv
论坛版主
帖子: 8273
注册时间: 2006-05-03 0:39
来自: المريخ
送出感谢: 0
接收感谢: 1 次

#6

帖子 stlxv » 2007-06-15 20:34

houdini 写了:
eexpress 写了:作什么的?能吃饭不
模型验证。

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

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

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

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

在网络协议里也有一些应用。
最终还是要通过数学方法来证明……
PHP是最好的语言!不服来战!
头像
kqueenc
帖子: 630
注册时间: 2007-05-27 20:29
送出感谢: 0
接收感谢: 0

#7

帖子 kqueenc » 2007-11-21 21:09

我们学校就用这个工具教学的。
因为……这个工具就是我们学校教研组开发的 :lol:
乖娃娃
帖子: 1
注册时间: 2008-03-24 14:39
送出感谢: 0
接收感谢: 0

#8

帖子 乖娃娃 » 2008-03-24 14:44

请问:UPPAAL可以在哪里下载?
回复

回到 “软件推荐”