《表4 子问题图的分解结果》

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

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

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

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

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

类似地，可以得到其他的7个子需求的情景图，限于篇幅，详见网址https://github.com/lxsbamboo/ZC-Verification.git.基于根据这些情景图，使用文献[19]中的基于情景的需求投影方法，将问题图5分解，得到8个子问题.每个子问题都对应解决一个子需求，有自己的子环境和子交互.这8个问题是类似的.以子问题P1为例，其用来对子需求R1进行验证，在待开发软件中，P1涉及到的子机器为M1，和M1进行交互的外部实体为子环境E1，包括Train、Block、Branch、Block Layout和Branch Layout，IS1为M1和E1之间发生的交互，其中，{int1，…，int9}为Train发送给M1的列车定位信息，{int12，…，int15}为Block发送给M1的Block逻辑分布，{int16，…，int18}为Branch发送给M1的Branch逻辑分布，{int19，…，int22}为Block Layout发送给M1的Block实体分布，{int23，…，int25}为Branch Layout发送给M1的Branch实体分布，{int10，int11}为M1经过计算后发送的EOA报文，int48为Train的报文接收状态.其他子问题详见表4.