周庭梁， 许 婧， 陈小红， 赵时旻

(1.同济大学 道路与交通工程教育部重点实验室， 上海 201804；2.卡斯柯信号有限公司， 上海 200071;3.华东师范大学 上海市高可信计算重点实验室, 上海 200062)



基于因果关系的列控系统模型约简方法

周庭梁1,2， 许 婧2， 陈小红3， 赵时旻1

(1.同济大学 道路与交通工程教育部重点实验室， 上海 201804；2.卡斯柯信号有限公司， 上海 200071;3.华东师范大学 上海市高可信计算重点实验室, 上海 200062)

在基于安全需求对验证问题进行投影的方法基础上，针对投影出的验证子问题，提出了基于因果关系的变量约简方法，定义了环境变量间的因果关系，归纳出基本的因果关系组合，并提炼出变量约简规则，通过变量约减减少了验证问题的状态空间.采用国内某地铁线路的相关数据进行建模和验证，结果表明，该方法能够有效降低系统验证复杂度.

需求验证； 变量约简； 因果关系； 列车运行控制系统

作为一种安全攸关系统，列车运行控制系统(简称列控系统)必须经过验证.目前列车运行控制系统的建模和验证方法主要有以下3种：① 基于逻辑的方法.这类方法基于集合论和一阶逻辑，采用逻辑推理或者定理证明的方式精化系统的功能，证明系统的正确性，典型代表是Z，VDM，B和Event-B方法[1]等，其中B方法已经在法国巴黎RER线路所采用的SACEM系统[2]中得到成功应用.② 基于进程代数的方法.进程代数关注并行行为，强调对不同模块并发过程之间的交互进行建模.例如，Zou等[3]调研了如何对CTCS-3(Chinese Train Control System 3)的系统需……