基于B方法的道岔控制系统形式化建模与验证

刘 宁，韩 程，王 峥，侯锡立，王恪铭

（1．西南交通大学唐山研究生院，河北唐山 063000；2．北京全路通信信号研究设计院集团有限公司，北京 100070；3．通号粤港澳（广州）交通科技有限公司，广州，511400；4．西南交通大学系统可信性自动验证国家地方联合工程实验室，成都 610031）

形式化方法是描述系统性质的基于数学的技术，指一类有严格数学语义的方法，它提供了一个可以在其中以系统的方式描述、开发、验证系统的框架[1]。人们使用具有精确语义的符号描述所要设计的软件系统，并对所描述的系统进行严格证明，可以揭示设计中的缺陷。通过使用形式化方法开发、验证系统，可以很大程度减少设计缺陷，提高系统的安全性[2]。

道岔控制系统（Point Control System，PCS）作为城市轻型轨道交通信号控制系统中分布式联锁子系统使用。目前已有大量学者将形式化方法运用在联锁系统的开发过程中[3-8]。以上研究针对系统的功能安全进行研究，尽可能减少系统设计缺陷，集中在系统需求分析阶段，而对形式化方法在系统需求分析阶段到代码实现阶段的应用研究不足，且缺少运用形式化方法开发PCS的研究。本文针对以上不足之处，尝试使用形式化B方法开发PCS，将系统建模、验证及编码等工作进行融合，推广形式化方法在国内的应用。

1 系统建模元素定义

本文技术路线如图1所示。基于需求规范，对系统建模元素进行定义，并结合模型架构对系统的功能逻辑进行B模型的建模工作，通过定理证明和模型检测两种技术手段对建立的B模型进行形式化验证，最终生成可执行的C代码。

图1 技术路线Fig.1 Technical route

为使非形式化的需求规范信息变得精确，用形式化的方式去描述该系统的非形式化规范，需明确系统的输入/输出消息以及各个消息可能取到的值等信息。本节通过定义变量、常量、静态数据及其关系描绘出系统的大致框架，便于后续的建模工作。

1.1 消息

PCS在运行过程中，不断采集外部设备的信息，经过一系列的逻辑判断，最终产生新的驱动命令驱动外部设备改变状态，以此来达到保证行车安全的目的。整理出这些消息有助于后续的建模工作。系统在循环工作中接收以及发送的部分消息如表1、2所示。

表1 部分输入消息Tab.1 Partial input information

系统在每次循环工作中存在的内部消息如表3所示。

表3 内部消息Tab.3 Internal information

1.2 集合和常量

本节定义在形式化建模阶段需要的静态数据，思想是将同一类状态归为一个集合。此外，静态数据还应包括一些表示命令的常量。下面定义一些单独的表示命令的常量，主要是一些命令表示信息，方便后续建模时使用，如表4所示。

表2 部分输出消息Tab.2 Partial output information

表4 表示命令的部分常量Tab.4 Partial constants for indication commands

1.3 系统静态数据关系

为了在建模时便于描述联锁表的各种数据，采用最简单、直接的方式，即将进路数据提前定义。对所有进路、信号机、道岔、区段从0开始进行编号，将其当作静态数据，放在单独一个抽象机中，方便其他模块在需要进路信息时参考。

此外，还需注意，一条进路对应的始端信号机只有一个，所以进路与信号机的数据关系可以用一维数组表示，如图2所示。

图2 进路与信号机的数据关系Fig.2 Data relationship between route and signal

进路与道岔、区段的关系比较复杂，一条进路会对应多个道岔、多个区段，所以进路与道岔、区段的数据关系需要用二维数组来表示，如图3所示。

图3 进路与道岔、区段的数据关系Fig.3 Data relationship between route and point, as well route and section

但还需注意，每条进路所包含的道岔数量也存在不相等的情况。为表示某条进路是否跟某个信号机、区段有关系，还需单独定义一个数据关系来表示，即判断进路与道岔、区段编号之间的关系是否为TRUE，若是，则说明该编号的道岔（区段）与该条进路有关联；若否，则说明该编号的道岔（区段）与该条进路无关联。

2 系统功能B模型建立

B方法作为软件开发方法，最初由J-R Abrial在1980年提出，其基本思想是提供一种表示方法，使用“抽象机记法”和“广义代换语言”来描述软件[9]，用它描述的软件最终可以用过程性的高级语言实现，甚至是汇编语言。该方法提供一个框架，在该框架中可以完善规范直至实现，可以将实现转换为C编程语言。B方法是第一个单一的形式化方法，涵盖了从规范到设计到实现的软件开发过程的所有阶段。

B方法的基础是集合论、关系代数和一阶谓词逻辑，他们都有严格的形式和精确的定义。使用B方法描述软件的基本单元是抽象机，该抽象机包括：数据描述（常量、变量）；操作描述（数据上的一组操作）；不变式（数据状态必须满足的一组关系）。

将对应道岔控制系统的规范描述和设计给出其形式化模型。从外界需要的系统接口，即外部操作人员需要的功能开始，建立一个非常抽象、不确定的系统规范模型，然后逐步精化，引入描述细节，由最开始的描述“做什么”到最终的描述“怎么做”。为便于描述，下面展示的形式化B模型是简化后的版本，该B模型基于单条线路建立，线路只涉及单个信号机、单个道岔、单个区段。

2.1 系统体系结构

系统完整的体系结构如图4所示（图中省去了SEES静态数据的内容）。

图4 系统体系结构Fig.4 System architecture

系统的体系结构，即模型框架，需要在建模前确定。因为要考虑到模块消息的交互，若模型框架不合适，模块之间无法有效的将信息交互，同时给后续的形式化验证工作带来不便。

2.2 机器文件PCS_Main

在该机器中描述了一些带有输入参数的操作，通过该机器提供的接口，外部工作人员就能够进行一些基本操作。这些操作不需要描述细节，只负责给外部提供一个接口，所有代换都用“skip”代替。机器文件PCS_Main包含的部分操作如表5所示。

表5 机器文件PCS_Main包含的部分操作Tab.5 Partial operations contained in “PCS_Main”

该机器中的操作示例如图5所示。在考虑该机器的抽象操作时，只描述了一个非常不确定的轮廓，甚至没有不变式，即这些抽象操作没有要维持的不变式，故该机器不会产生证明义务。

图5 机器文件PCS_Main的部分内容Fig.5 Partial “PCS_Main” representation

2.3 机器文件PCS_Main的实现

区别于分解操作的实现方式，基于机器文件PCS_Route和机器文件PCS_Input实现机器文件PCS_Main的基本想法是利用机器文件PCS_Input中一些查询操作的输出信息和机器文件PCS_Route中的部分操作来实现机器文件PCS_Main中的相应操作，如图6所示。

图6 机器文件PCS_Main中操作Route_Operation的部分实现内容Fig.6 Partial “Route_Operation” implementation in “PCS_Main”

显然，该操作的实现相比于规范描述显得很复杂，不但用到被导入抽象机的操作，还用到VAR…IN…结构，IF结构嵌套。该操作描述了进路控制过程，包括进路选排、进路锁闭、信号开放与信号保持以及进路解锁。具体过程：进行进路操作时，先调用操作UPDATE_ROUTE_CONDITION_FUN和操作CHECK_POINT_POS，用来判断进路选排条件是否满足，其中操作UPDATE_ROUTE_CONDITION_FUN和操作CHECK_POINT_POS的保卫条件与执行语句根据相应需求文档得到。若进路选排条件满足，则执行进路选排操作，并且再次调用上述两个操作，判断进路锁闭条件是否满足。如果进路锁闭条件满足，则执行进路锁闭操作，同时调用操作SIGNAL_FILAMENT_QU判断信号开放条件是否满足。若信号开放条件满足，则进行信号开放，并且调用操作SECTION_STATUS_QUERY_FUN判断进路上区段的状态信息，即进路解锁的检查条件。若满足此条件，则执行进路解锁操作。

2.4 机器文件PCS_Route

机器文件PCS_Route是PCS模型的主要部分，系统的主要运行逻辑都在该机器中被描述。除了描述人工控制道岔、信号机状态的操作接口，还描述了进路控制过程的各个阶段的操作接口。部分抽象变量如表6所示。

表6 机器文件PCS_Route中定义的部分抽象变量Tab.6 Partial abstract variables defined in “PCS_Route”

该机器文件中包含的部分操作如表7所示。

表7 机器文件PCS_Route中定义的部分操作Tab.7 Partial operations defined in “PCS_Route”

相较于机器文件PCS_Main描述的抽象操作，机器文件PCS_Route中描述的部分抽象操作更为复杂，如图7所示操作中，用到ANY...WHERE...THEN...结构，其目的是基于道岔、区段、信号机的任意选择来描述一系列进路选排条件的检查，之后执行的变量Check_Condition_Result的赋值动作都依赖于此任意值。

图7 操作UPDATE_ROUTE_CONDITION_FUN的代码Fig.7 Code of operating “UPDATE_ROUTE_CONDITION_FUN”

3 系统属性验证及代码生成

形式化语义符号描述了系统，更重要的是要对系统的性质和安全性进行严格的证明，通过证明过程，揭示系统设计中的潜在缺陷。此外，将通过验证后的B模型生成C代码也是本节的目标。

3.1 安全属性验证

本小节主要围绕形式化验证展开，即通过将系统的安全属性描述为不变式（invariant），以此来约束系统的常量、变量之间的关系，保证系统状态的改变都是在规定的范围内，从而确保系统运行过程的安全性。

现有安全属性SRS-1：当道岔处于解封状态时，才可转动道岔。将其转换为不变式如公式（1）所示。

此时该不变式产生的关于操作POINT_ROUTE_UNBLOCK_FUN的证明义务未通过。原因是操作POINT_ROUTE_UNBLOCK_FUN的代换语句中会改变Point_Block_State的值，故需要证明在该变量值改变后仍然能够维持不变式所描述的静态规则。在操作POINT_ROUTE_UNBLOCK_FUN中添加一个前条件Point Pos : {PCS_POINT_NORMAL,PCS_POINT_REVERSE}，上述证明义务成立。

上述模型共计生成154条证明义务，通过完善模型中的形式表达，以及结合手动交互式证明策略，最后所有生成的证明义务都证明通过。证明义务统计情况如图8所示。

图8 模型的证明情况统计Fig.8 Proof statistics of the model

3.2 代码生成

Atelier B支持将形式化B模型转换为高级编程语言，使得形式化B方法贯通软件系统开发的全过程。排列某条进路的场景如图9所示，当进路排列后，信号机灯丝工作正常，则可以开放信号机；但在执行解锁进路时，输入区段被占用的信息，则进路无法解锁。C代码的运行结果满足此需求。

图9 代码运行情况示例Fig.9 Demonstration of code running

4 总结

本文基于PCS的需求规范，整理出系统各模块的建模元素，用形式的方式描述系统的非形式化的规范，使用形式化B方法以自顶向下的方式进行系统原型设计开发，将形式化方法应用于系统需求分析至最终的代码实现阶段，得到以下主要结论。

1）对系统的功能逻辑建立形式化模型，实现对系统的需求规范、系统功能及决策过程的验证，提高了系统模型的质量。

2）通过这种开发方式，将验证后的系统模型生成可执行代码，减少了编码阶段的工作量，间接减少测试反馈修改的工作量。