UPPAAL
发布人:上海迪真计算机科技有限公司       


UPPAAL是基于时间自动机的系统行为建模、仿真、模型验证检查工具。


优势:

  • 在传统有限状态机模型描述基础上,描述实数域语义的时间变量;
  • 支持对安全性、可达性、必然性、潜在性四大设计需求的形式化描述和快速模型验证
  • 验证算法速度极快;
  • 在任务苛刻型、安全苛刻型系统中得到广泛应用,快速验证是否存在系统死锁;
  • 与主流建模开发工具有接口。


 

 通过使用UPPAAL可以很好的解决目前实时应用系统设计阶段中最核心的分析验证问题,配合目前的以人工评审、仿真手段增加形式化的建模分析验证手段来保证对系统行为进行更深入的分析验证,最终能够提高整个系统的正确性、安全性、可靠性质量。


UPPAAL实施步骤:

1、模型建立或导入


    UPPAAL提供图形化自动机建模与类C语言的数据结构描述与类C语言的控制算法描述三者结合的方式来描述系统行为及可能存在的时间约束。将系统行为抽象为若干个自动机,定义可能的各自动机内部构造及与其它自动机的同步。

2、仿真运行

    UPPAAL在检查模型的基本语法无误后可进行人工单步仿真或者鲁棒性随机自动仿真,可以将仿真运行序列存入文件供以后运行。

3、设计需求形式化描述及验证

    将设计需求用CTL逻辑语言表达式进行描述。


软件模块:


成功案例:


-AirBus Control Panel子系统测试验证

-AirBus ACS子系统测试验证

-银行分布式交易系统测试验证

-Xilinx Virtex-4 4VFX12多任务计算系统利用率优化验证

-EKC控制系统测试验证

-NASA 深空一号远程代理自治系统的任务规划及调度机制验证

-Honeywell AFDX冗余机制及算法验证

-Honeywell TCAS III防空中碰撞航向偏离策略验证  

-Boeing787 AADL系统体系架构验证  

-NASA 音视频通讯控制器电源控制逻辑验证

-国内某箭机三模冗余系统的设计参数验证

-WSN无线传感网络系统电能消耗优化验证

-雷达信号接口卡内存仲裁机制验证

-Saabcentral lock system系统验证

-基于OSEK/VDX的应用程序验证

-瑞典Mecel AB公司变速箱控制器(GEAR BOX CONTROLLER)仿真验证