《表1 待验证属性与CTL描述说明》

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

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

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

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

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

根据CTL语句特点，结合本文验证目标，即得到满足场景需求且符合系统规范的场景方案，定义五类主要属性：可达性、活性、转移性、确定性和互斥性。其中，可达性和活性保证功能的可实现性，主要用于验证场景的功能性需求。转移性和确定性验证场景过程是否按照设计进行，以及场景中的交互行为是否符合系统规范。互斥性主要验证场景实现的安全性需求，如确保系统状态相互不冲突，在规定地点（区域）完成等。属性的具体含义和相应的CTL语句见表1。