《表3 BNF验证语句含义表》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《C3+ATO系统模式转换功能建模与仿真验证研究》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

UPPAAL是基于时间自动机的形式化建模与验证工具，包括编辑器、模拟器、验证器三部分。编辑器可以创建模型并进行相关变量定义，模拟器可以用来检验所建模型是否有语法错误并且生成不同流程对应的消息顺序图，验证器可以用来验证模型是否满足相应的功能性质。建立模型后，模型的验证主要将C3+ATO系统技术规范中功能属性转化为对应BNF验证语句进行检验。BNF验证语句根据路径表达可分为3种：可达性、安全性、存在性，验证语句含义见表3。