《表2 主要属性与验证结果》

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

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

《CTCS-1级列控系统等级转换场景建模与验证》

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

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

验证开始后，系统先后验证NuSMV模型是否符合语法规则和满足系统属性。验证语法规则时，根据系统报错逐一修改即可。验证系统属性时，根据反例定位错误原因。可能的原因包括状态转移条件有遗漏、转移关系逻辑有误（矛盾），以及模型元素误写等。经过反复修改与验证，最终所有属性验证通过（返回值为true），即验证了完善后的场景方案是满足场景需求且符合系统规范的。由于验证属性较多，不一一列出，主要属性及验证结果如表2所示。