基于混合通信顺序进程高速铁路列控系统形式化建模与验证方法

《基于混合通信顺序进程高速铁路列控系统形式化建模与验证方法》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第33卷，第5期中国铁道科学V01．33No．52O12年9月CHINARAILWAYSCIENCESeptember，2012文章编号：1001—4632(2012)050091一07基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法吕继东1，李开成1，唐涛2，袁磊2(1．北京交通大学轨道交通运行控制系统国家工程研究中心，北京100044；2．北京交通大学轨道交通控制与安全国家重点实验室，北京100044)摘要：针对高速铁路列控系统的混杂特性，提出一种基于混合通信顺序进程(HCSP)的列控系统形

2、式化建模与验证方法。引入了HCSP的假设条件，建立列控系统的行为模型；定义了HCSP到混合自动机(HA)的转换规则，将HcsP模型转换成HA模型；利用模型检验工具PHAVer对HA模型进行自动验证。以高速铁路列控系统典型的行车许可运营场景为例，建立区间闭塞分区行车许可场景的HCSP模型；根据转换规则将行车许可场景的HCSP模型转换成HA模型；用PHAver验证了所建立的区间闭塞分区行车许可场景模型的正确性，从而证明了基于HCSP的高速铁路列控系统建模及验证方法的有效性。关键词：高速铁路列控系统；混合通信顺

3、序进程；混合自动机；行车许可场景中图分类号：U284．482；U238文献标识码：Adoi．10．3969／j．issn．1001—4632．2012．05．14高速铁路列控系统是一个典型的混杂系统[1]。SequentialProcess，CSP)[8]的推广，可用来描述各国学者采用不同的形式化方法研究了列控系统的混合系统的行为。HCSP中的连续构件可以表示一混杂性[2。6]。但均没能很好地描述列控系统中子系个具体给定初值的微分方程，离散构件中的顺序算统之间的离散事件交互过程。针对列控系统混杂性子、条件

4、算子等则可以刻画连续构件和通信间的耦的研究，要精确的形式化方法描述列控系统的行合关系。因此，采用HCSP能够对高速铁路列控为，不仅要考虑物理实体的连续演变过程(如列车系统进行精确的形式化建模，不仅能够刻画列控系的速度、位置等)，还要考虑子系统之间离散事件统中连续演变过程，而且能够刻画子系统之间离散的交互过程。因此，本文针对高速铁路列控系统的事件的交互过程。由于目前还没有一套完整的混杂性，提出一种基于混合通信顺序进程HCSP[7]HCSP模型验证方法，本文通过引入HCSP的2个(HybridCommunic

5、atingSequentialProcess，HC—假设条件，结合HA理论，提出HCSP到HA的SP)的列控系统形式化建模与验证方法。通过定转换规则，将HCSP模型转换成HA模型，利用义HCSP到HA的转换规则，将HCSP模型转换模型检验工具PHAVer对HA模型进行自动验证。成HA模型，并利用模型检验工具PHAVer进行1．1基本假设HA模型的自动验证。以高速铁路列控系统典型的由于HCSP中通信过程和赋值语句都消耗时行车许可运营场景为例，采用该方法对区间闭塞分间，那么进程夕会终止￡个单位时间(通信过程和

6、区行车许可场景进行建模与验证分析，结果证明了赋值语句的时间)，并且给后期模型的验证带来了该方法的有效性。一定的困难，因此做如下假设。(1)赋值语句不消耗时间(赋值语句的时间远1HCSP建模和验证方法远小于真实物理过程的处理时问)；(2)通信同步过程不消耗时间，但通信的等待HCsP是通信顺序进程(Communicating收稿日期：2011一08—20；修订日期：2012一02一16基金项目：国家“八六三”计划项目(2011AA010104)；北京交通大学轨道交通控制与安全国家重点实验室开放课题(R(洛20

7、儿KOl0)；北京交通大学科技基金资助项目(2012JBM024)作者简介：吕继东(1981)，男，河北廊坊人，讲师，博士。92中国铁道科学第33卷时间依然存在。(1)状态集合：状态集合为{‰，口t)，初始1．2转换定义位置为‰。根据混合自动机理论，定义转换函数西：(2)变迁集合：在初始状态下，不变量条件B(V)×B—m衄。其中，V表示HCSP中的所有加口(‰)=true，变迁流条件∥o叫(矶)一true，发变量，B(V)表示V的1个映射函数，HAf嘲表示混生瞬时事件E，混合自动机由初始状态砺变迁到状合自

8、动机的1个片段(fragment)，其定义如下态u1。如图1所示，其中，舭趔(E)一true，HAf唧=(、厂，‰，拥勘，∥o叫，面九P，E，田“rce，耻挖￡(E)一f，如优p(E)=(z，z—P)，￡arg西，g獬，d，J“，n户，三，疚圯咒￡)鼢“rce(E)=矾，缸rg以(E)一vl。(1)式中：‰表示片段的初始位置；i刀口表示不变量谓词；∥o硼表示流谓词；如，le表示状态谓词；E表示事件集合；sD“rfe表示源谓词；