基于安全状态机的RBC系统行车许可模块的建模与验证的中期报告.docx

基于安全状态机的RBC系统行车许可模块的建模与验证的中期报告

引言

铁路列车的行车许可系统是铁路列车运行的重要组成部分，通过该系统，控制铁路列车在装备站、停车场、车站等地驶入或驶出。在这个系统中，RBC（RadioBlockCenter）是实现行车许可的关键组件之一。

为了保证RBC系统的安全性与可靠性，本文采用基于安全状态机的方法对RBC系统行车许可模块进行建模与验证，并在建模过程中着重考虑了系统的安全性、实时性和可靠性。

建模与验证方法

基于安全状态机的方法是一种常用的建模与验证方法，其主要思想是将系统中所有可能的状态及其转移关系描述成状态图，并且在状态图中加入相应的安全属性，以此来保证系统在运行过程中满足安全性要求。

具体地，本文采用了UML建模语言对RBC系统行车许可模块进行建模，并在UML状态图中加入了相应的安全属性，包括：

1.系统状态：描述系统中所有可能的状态。

2.系统事件：描述在系统运行过程中可能会发生的事件。

3.系统转移关系：描述系统状态之间的转移关系。

4.安全属性：描述系统在运行过程中需要满足的安全性要求，包括不变式、前置条件、后置条件等。

在建模的过程中，需要对RBC系统行车许可模块进行详细的分析和设计，包括状态的定义、事件的定义、转移关系的定义、安全属性的定义等。

基于建模结果，可以通过模型检测技术对RBC系统行车许可模块的功能性和安全性进行验证，以此来发现系统中可能存在的错误和安全隐患。

实验结果

在实验中，我们针对RBC系统行车许可模块进行了建模和验证。基本的建模元素包括状态、转移关系、事件和安全属性等，其中安全属性主要包括前置条件、后置条件和不变式等。

我们设计了一个包含4个状态和4个事件的状态图，其中的状态包括：

1.初始化状态

2.配置状态

3.计算状态

4.发布状态

同时定义了相应的事件，包括：

1.初始化事件

2.配置事件

3.计算事件

4.发布事件

基于UML状态图和安全属性的定义，我们采用模型检测技术对系统进行验证。通过验证，我们发现RBC系统行车许可模块满足安全要求，不存在安全隐患，同时保证了系统的实时性和可靠性。

讨论与结论

本文采用基于安全状态机的方法，对RBC系统行车许可模块进行了建模与验证。通过实验结果表明，该方法可以有效地开发和测试RBC系统中的行车许可模块，并且保证了系统的实时性和可靠性。

在今后的研究中，我们将进一步优化建模和验证方法，发现更多的安全隐患和错误，并加入更多的安全属性，以此来提高系统的安全性和可靠性。