《表5 验证试验结果：基于模型检验的需求不一致研究》

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

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

《基于模型检验的需求不一致研究》

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

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

属性规约是系统运行过程中必须满足的规范，其保证了系统的一致性和安全性。针对于本文提到模型，主要从以下几个方面进行验证：（1）安全性。一个系统的运行首先要保证其安全性，对此要验证的是：在未来的任意一个时刻，电梯系统都不会把乘客困在电梯中。（2）前向一致性。电梯系统的运行需要满足前向一致性。对此验证电梯初始状态为空闲状态时，当有乘客进入时，未来的某一状态会由于超重导致电梯报警。（3）可达性。对此要验证电梯系统的自动机模型是否可以到达任何一个图中描述的状态。（4）陷阱性质。根据自动机图中描述的状态变迁，人为增加一条和某一行为需求描述相似的变迁，对其进行取反操作，观察模型检验能否检测出相似且不一致的行为。对此要验证当有乘客在一楼且按下上行按钮后，电梯不会出现上行状态。检测结果见表5。