《表1 从需求问题到需求验证模型静态视图的构造规则》

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

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

《区域控制器的安全需求建模与自动验证》

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

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

根据上述描述，我们设计了需求验证模型的自动构造规则，见表1.该转换规则是根据需求问题P自动生成为需求的验证模型，从P中读取机器M来构建验证机器VM；根据需求的验证结果来构建验证报告VR，E′为环境E、机器M和验证报告VR的并集；根据IS中交互来构建IS′中新的交互:交互的发送方为原来的交互发送方交互的接收方为验证机器VM，交互的内容与原来的交互内容相同；另外，新建与验证报告之间的交互:交互的发送方为验证机器（VM），接收方为验证报告（VR），内容包括验证结果（bValid）和验证失败时需要提供的反例（cExample）.