RBC切换协议的建模与验证：CTCS-3安全关键系统的正确性验证

可在www.sciencedirect.com在线获取理论计算机科学电子笔记309（2014）51-62www.elsevier.com/locate/entcsRBC切换协议的建模与验证杨凯1，2西安电子科技大学计算理论与技术研究所、ISN实验室中国段振华、丛天3西安电子科技大学计算理论与技术研究所、ISN实验室中国摘要无线闭塞中心（RBC）是中国列控系统3级（CTCS-3）的核心部分，安全关键系统的协议RBC切换协议的正确性是影响系统安全性的重要因素之一。 因此，确保其正确性是非常重要的。的协议。为此，一些形式化的方法已被用来建模和验证协议。在本文采用建模、仿真和验证语言MSVL作为协议的形式化语言，对协议进行了建模和验证。结果表明，RBC切换行为符合规范要求。关键词：CTCS，RBC切换，建模，验证1介绍CTCS-3是我国铁路正在开发的、具有安全性要求的列控系统协议。CTCS-3的系统需求规格书是用自然语言编写的，不可避免地包含歧义和缺陷。需求规格说明中的模糊性和缺陷可能导致整个系统开发的失败。在安全关键的情况下，故障可能是致命的1本研究得到国家973重点基础研究项目（项目编号：2010CB328102）和国家自然科学基金项目（项目编号：2010CB328102）的资助。的基金号61133001、61272117、61272118、61202038、91218301、61322202和61373043。* 对应作者所有2电子邮件地址：kaiyang@stu.xidian.edu.cn3邮箱：zhhduan，ctian@mail.xidian.edu.cnhttp://dx.doi.org/10.1016/j.entcs.2014.12.0051571-0661/© 2014作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/3.0/）。52K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）51系统. 因此，需要高质量的规范，这些规范应满足质量属性，例如正确性，完整性，一致性和可追溯性[16]。为了更形式化地描述需求，通常使用统一建模语言（UML）对系统需求规格说明进行建模。UML作为一种可视化的建模语言，在系统建模方面具有一定的优势，自诞生之日起就成为一种流行的建模语言。为了充分利用UML的特点，许多工具（RationalRose，ArgoUML，Rhapsody等）都可以在UML中使用。 必须利用市场上存在的资源来支持其功能。然而，不幸的是，它们都不能保证规范的正确性[1]。因此，已采用形式验证方法来验证系统是否满足所需属性。事实上，许多其他的研究已经做了形式化的分析RBC切换与不同的方法。在文献[12]中，作者使用微分动态逻辑对欧洲列车控制系统2级（ETCS-2）的RBC切换进行了建模和验证。根据红细胞切换协议，作者简要概括了红细胞切换行为，并建立了一个形式化模型，成功地描述了红细胞切换行为。此外，他们提出的避免碰撞和避免脱轨的要求都通过最终验证得到满足。在文献[2]中，基于消息序列图对ETCS-2的RBC进行了形式化建模和验证。利用随机Petri网[15]建立了ETCS-2在两种不同列车配置下的切换失败概率模型，并分析了不同列车速度和RBC重叠对RBC切换成功概率的影响在文献[11]中，Faber等人使用形式化语言CSP-OZ-DC描述了ETCS-2的RBC规范，并给出了将模型转换为PEA后的模型检查和推理验证方法。投影时序逻辑（PTL）[3，4，10]是系统验证的有用形式。MSVL [7，8，5]是PTL的可执行子集，可用于建模，模拟和验证并发系统。为此，系统被建模为MSVL程序，并且系统的属性由命题投影时序逻辑（PPTL）公式指定。因此，系统是否满足该属性可以通过具有相同逻辑框架的模型检查来检查[6，9，17]。此外，异步通信技术已经在MSVL中实现，因此，MSVL可以用来建模异步分布式系统[14]。在本文中，我们使用MSVL作为形式化语言的RBC切换协议的建模和验证协议的一些性质本文其余部分的结构如下。第二节简要介绍了MSVL的MSV工具包。RBC切换协议在第3节中描述。第4节和第5节致力于协议的建模、仿真和验证。最后，在第六节给出了结论K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）51532MSV工具包MSVL语言是具有框架技术的投影时态逻辑的子集[8]。开发了一个名为MSV的工具包，工具包的结构见图1。正如其名称所示，MSV工具包可以在三种模式下工作：建模，仿真和验证。仿真模式下，程序中的变量在每个状态下的值被评估并输出，而建模模式下，程序的模型被给出。用户可以在验证模式下输入PPTL公式描述的属性，MSV工具包将自动检查系统是否满足该属性。如果不满足该特性，MSV工具包将给出所有反例，系统设计人员可以根据反例修改系统。核查过程见图2。此外，在[14]中给出了进程结构、通道结构和通信命令的形式化定义，这使我们能够对具有异步通信的并发系统进行预NF坐符号表程序编辑器属性编辑器验证MSVL程序PPTL公式语法树建模简化词法分析器代币代币解析器解析器仿真树输出视图NFG图1.一、MSV工具包的结构3CTCS-3的RBC切换协议3.1CTCS-3的结构在介绍RBC切换协议之前，我们首先简要介绍了CTCS-3的结构。CTCS-3主要由三个子系统组成，如图3所示，即车载子系统、地面子系统和网络通信子系统。RBC作为CTCS-3级CTCS-3的核心地面子系统，其主要任务是保证列车运行的安全性和效率。SMCBMCAMCUMC54K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）51*URXQGHTXiSPHQW（0）公司简介HTXiSP HQW（i）（5%公司简介HTXiSP HQW（i+1）（%（i+1），*URXQGHTXiSPHQW（Q）我6%1%6&+DQGRYHU =RQH%761%761&RYHUDJH=RQH%76²&RYHUDJH=RQH%76²7UDiQ²7UDiQ 1%DOiVH+DQGRYHU3RiQW*60-56\VWHP3URSHUW\069/3URJUDP（M）337/）RUPXOD（P）069IQWHUSUHWHU/1）* RIP6DWiVIiHG2019 - 01 -2500：00：001RW6DWiVIiHG（RXQWHUH[DPSOH图二. MSV工具包铁路信号系统的故障安全原则。RBC使用来自其他子系统的信息来计算实时移动权限（MA），并将MA转发给由其控制的列车图三. CTCS-3的结构RBC子系统包括通信模块（无线信息处理模块和地面信息处理模块）、控制模块（列车控制命令和列车运行间隔管理）和MA计算模块[13]。3.2RBC切换协议由于单个RBC的控制能力有限，多个RBC被放置在铁路沿线。当列车到达当前RBC的控制区域边界时，列车的控制应移交给下一个RBCK. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）5155(QG RI 0$0美元%DOiVH*URXS0美元7UDiQIQIRUPDWiRQHWF.5% 15%²5RXWHIQIRUPDWIRQHWF.该过程称为RBC切换，如图4所示。在正常情况下，程序自动完成，不需要驾驶员红细胞移交包括两种情况：1.RBCRUGHU %5RXWHIQIRUPDWIRQIURP5%15RXWHIQIRUPDWIRQIURP5%²7UDiQ见图4。 RBC切换与两个普通广播电台交接;2.红细胞移交与只有一个正常的电台。两种情况下的移交程序不同。我们在这里集中讨论第二种情况。我们使用RBC 1表示切换RBC，RBC 2表示接管RBC。RBC与一个正常无线电台的切换过程如下：1) 列车通过等级转换通告应答器组（LTA）进行RBC转换后，列车向RBC 1发送位置报告2) 当RBC 1收到列车的位置报告时，向列车发送RBC转换命令（消息包131），向RBC 2发送进路请求信息;3) 如果在RBC 2的区域中存在可用的路由，则RBC 2将向RBC 1发送混合移动权限，或者它将向RBC 1发送消息4) RBC 1根据来自RBC 2的信息，向列车发送扩展消息5) 列车前端（最大安全前端）通过过渡边界后，列车向RBC 1发送位置报告;6) RBC 1将位置报告转发给RBC 2;7) RBC 2收到RBC 1的位置报告后，向RBC 1发送接管信息;8) 列车尾部通过过渡边界后，向RBC 1发送位置报告;9) 根据列车提供的位置报告，当RBC 1检测到列车后端（最小安全后端）已通过RBC 1/RBC 2过渡边界时，将命令列车关闭与RBC 1的通信会话10) 列车收到RBC1的断开命令后，将断开与RBC1的通信。列车根据先前来自RBC1的命令开始呼叫RBC2 。如果呼叫成功，列车向RBC 2发送初始化信息（M155），RBC 2向列车发送通信版本信息（M32），列车发送通信建立信息56K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）51（M159）至RBC2。 然后，建立通信;以及11) RBC 2生成MA并将MA发送给列车。因此，完成从RBC 1到RBC 2上面的叙述性文字描述是非常多余的，不直观，但详细。它致力于支持和解释系统需求规范中的图形和表格形式。我们使用UML序列图对“RBC切换”过程进行建模。UML序列图是一种行为图，它是一种简单的、表达性的、直观的、图形化的和标准化的符号，用于指定在许多不同情况下系统实体之间的交互与类图和用例图一起，序列图是UML中最流行的图。序列图的表达性确保了系统的模型和规范之间的一致性[16]。UML序列图建模方法将场景的交互实体和事件发生映射到序列图的参与者（在UML1.x中称为对象）和消息。建模步骤如下所示(1) 列出场景中交互的所有实体（包括系统组件）(2) 找出所有事件的发生和场景实体之间的关联;(3) 将方案的基本元素（包括实体、事件发生和关联）映射到序列图;以及(4) 检查场景和序列图之间的一致性。按照所列步骤，我们构建了“RBC切换”场景的序列图模型图5中的消息的含义在表1中指示。4仿真与建模在前一节中给出了RBC切换过程的UML序列图。在本节中，我们将序列图转换为MSVL程序。RBC切换过程中有三个主要组成部分：TRAIN、RBC 1和RBC 2。它们是并行运行的独立分布式组件。对应于每个组件，我们定义一个过程。这三个过程是平行的，它们之间有一个沟通渠道。火车的状态会根据它收到的信息而改变。正常情况下（无消息丢失）的仿真结果如图6所示。程序中各变量的含义见表二、在最后一个状态中，变量“HandshHandover”的值我们在建模模型下使用MSVL工具包运行程序，所有执行路径如图7所示。由于路径太长而无法在图中完全显示，因此仅显示部分路径。图7中的两条路径分别代表两种情况：1.RBC移交程序完成K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）5157表1图5中消息的含义消息含义RBC切换命令请求列车信息路由请求信息呼叫通信初始化信息路由器呼叫通信版本信息CommBuilt通信内置信息路由器RBC路由信息HybridMA边界上的Hybrid MA列车位置列车的位置arriveRN火车的前端到达边境安进入RBC 2区域Infor收购信息MA运动当局passRN列车尾部通过边境关闭通信终止通信表2程序中变量的含义变量含义消息列车消息列车接收消息RBC1消息RBC1接收消息RBC2消息RBC2接收级别列车SupervisedByRBC 1列车由RBC 1监控SupervisedByRBC 2列车由RBC 2监控CommBuilt与RBC 2建立通信成功完成RBC切换过程58K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）517UDiQ5% 15%²1： 3DVV/7$²：5%RPG3： 5HT7UDiQBIQIRU4：$QVZHU5%&5：+\EUiG0$6：7：7UDiQBSRViWiRQ8：$UUiYH51第九章$QQ10：3DVV51十一岁1²：DOO13：$QVZHUDOO第15章：我是你16：0$图五、RBC切换时序图见图6。 仿真结果成功; 2。RBC 2区域内无MA，列车控制级别最终变为2级。5验证本节给出了系统需求规范中规定的属性的验证过程在验证属性之前，我们需要用PPTL公式来指定它们。然后，可以通过以下方式K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）5159见图7。 建模结果使用MSV工具包进行模型检查。 在这里，我们只验证三个属性。属性1：最终RBC切换程序成功完成，或列车控制级别变为2级定义p：切换切换=1;定义q：级别=2;finn（p或q）特性2：列车向RBC1发送“PassRN”消息后，收到RBC1的“Close Comm”消息定义p：MessageRBC 1 =验证结果表明，上述两项性能均满足要求，但图8仅显示了性能1的验证结果。现在，我们验证第三个属性。结果如图9所示。从结果中我们可以看出，性质3不满足。该结果意味着列车在切换过程中的一段时间内既不处于RBC 1的控制下，也不处于RBC 2的控制下。在对需求规范进行分析后，我们发现当列车收到来自RBC1的消息“关闭通信”时，与RBC1的通信将断开（时间1）。然后，列车开始呼叫RBC 2，直到与RBC 2建立通信（时间2）。 在时间1和时间2之间，列车既不受RBC 1也不受RBC 2监督。因此，属性3的验证结果与要求规范一致特 性 3 ： 列 车 始 终 处 于 RBC 1 或 RBC 2 的 控 制 之 下 定 义 p ：SupervisedByRBC 1 =1;60K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）51见图8。 物业1见图9。 物业3定义q：SupervisedByRBC 2 =1;always（p or q）K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）51616结论本文分析了CTCS-3级的RBC切换协议。根据需求规范，给出了切换过程的半形式化描述UML序列图然后，我们将半形式化的描述转化通过这种方式，不仅可以使用MSV工具包完成模拟和建模过程，而且可以完成更重要的过程，即，可以对协议进行验证。然而，从UML序列图到MSVL程序的转换是手工完成的。因此，很难保证两种形式之间的一致性。为了改善这一点，应该研究自动翻译方法。此外，未来还需要考虑模型中的引用[1] Beato，M. E、M. 巴里奥-索洛尔扎诺角E. Cuesta和P. delaFue nte，Uml自动验证tool与形式化方法，理论计算机科学电子笔记127（2005），pp. 三比十六[2] Chiappini，A.，A.奇马蒂角波尔齐亚湾罗通多河P. Traverso和A. Villa Fiorita，安全关键型列车管理系统的正式规范和开发，载于：计算机安全，可靠性和安全性（1999），pp. 410-419[3] Duan，Z.，“一个扩展的时间间隔时序逻辑和时序逻辑编程的框架技术.”博士论文，泰恩河畔纽卡斯尔大学（1996年）。[4] Duan，Z.，[5] Duan ， Z. ， M. Koutny 和 C. Holt ， Projection in Temporal Logic Programming ， in ： LogicProgramming and Automated Reasoning，Springer，1994，pp. 333[6] 杜 安 Z. 和 C. Tian ， A unified model checking approach with projection temporal logic ， in ： FormalMethods and Software Engineering（2008），pp. 167-186.[7] Duan，Z.，X. Yang和M.Koutny，框架时序逻辑程序的语义，在：逻辑编程（2005年），第页。356-370。[8] Duan ， Z. ， X. Yang 和 M. Koutny ， Framed temporal logic programming ， Science of ComputerProgramming70（2008），pp. 31比61[9] Duan ， Z. ， N. Zhang 和 M. Koutny ， A complete proof system for propositional projection temporallogic，Theoretical Computer Science497（2013），pp.84[10] 段志- H.和M. Koutny，A framed temporal logic programming language，Journal of Computer Scienceand Technology19（2004），pp.341-351[11] Faber， J.， S. Jacobs 和V. Sofronie-Stokkermans， 具 有复 杂数 据类 型和 时序 参数 ， 集 成形 式方 法，Springer，2007年，第100页。233-252。[12] Liu，Y.， T. 唐，J.刘，L. Zhao和T. Xu，RBC切换的形式化建模与验证自治分散系统（ISADS），2011年第10届国际研讨会，IEEE，2011年，pp. 六十七比七十二[13] Lv，J.和T. Tang，使用uppaal对，在：CSIE 2009，2009 WRI世界计算机科学与信息工程大会，3月31日-2009年4月2日，洛杉矶，加利福尼亚州，美国，IEEE计算机协会，2009年，pp. 49比53[14] Mo ， D. ， X. Wang 和 Z. Duan ， Asynchronous communication in msvl ， in ： Formal Methods andSoftware Engineering（2011），pp. 82比97[15] 纽河，Y. CAO和T. etcs层rbc切换协议的形式化建模与分析2使用随机Petri网，中国铁道学会学报4（2009），pp. 52比5862K. Yang et al. /Electronic Notes in Theoretical Computer Science 309（2014）51[16] 唐，W.，B.宁氏T. Xu和L.赵，CTCS-3系统需求规范的基于场景的建模和验证，在：计算机工程与技术（ICCET），2010年第2届国际会议，IEEE，2010年，第10页。400-403[17] 张 ， N. ， Z. 段 角 ， 澳 - 地 Tian 和 D. Du ， A formal proof of the deadline driven scheduler in pptlaxiomatic system，Theoretical Computer Science（2013）.URLhttp://dx.doi.org/10.1016/j.tcs.2013.12.014