赵晓宇 , 程瑞军, 程 雨, 马小平,4

(1. 中国铁道科学研究院 研究生部，北京 100081； 2. 北京交通大学 轨道交通控制与安全国家重点实验室， 北京 100044；3. 中国铁道科学研究院 基础设施检测研究所，北京 100081； 4. 北京交通大学 交通运输学院，北京 100044)

列车运行控制系统既包含连续的运行过程，又包含有离散的控制行为，属于典型的混成系统[1]。各国学者采用不同的形式化方法研究了列控系统的混杂性[2-6]，但均未讨论过含有未知控制参数的混成模型。然而，在系统开发的初始阶段，如何根据系统的安全性需求分析得到系统控制参数之间所满足的约束集，对系统安全显得尤为重要。因此，本文针对高速铁路列控系统，提出一种基于混成统一化建模语言HUML(Hybrid Unified Modeling Language)的列控系统形式化建模与参数分析方法。通过定义HUML到HYTECH模型的转换规则，将HUML模型转换成HYTECH，并运用模型检验工具HYTECH对模型的状态可达性进行验证。然后将安全性需求加入到满足可达性验证的模型，建立安全HYTECH模型，通过计算该模型的可达集，得到未知控制参数所需满足的约束集。最后，以移动闭塞中的追踪模型为例，采用该方法对列车的距离控制器进行建模和分析。通过分析得到控制参数的取值范围，对所得参数的验证结果表明该方法的有效性。

1 基于HUML模型的控制参数分析方法

基于HUML模型的控制参数分析方法基本流程见图1。具体步骤为：

Step1根据系统的需求规范或者协议文件，通过合理抽象并运用混成UML概要文件，建立系统的模型。……