铁路信号安全关键软件形式化建模

Formal Modeling of Railway Signal Safety Critical Software

针对现行建模方法不能满足铁路信号系统安全关键软件的时钟约束需求和模型复杂度较高的问题,分析SyncCharts建模方法,针对其缺少形式化规范和时钟约束的问题,扩展出具有时钟属性的Timed SyncCharts建模方法。首先,采用Z语言系统地给出了Timed SyncCharts的形式化定义;其次,结合Timed SyncCharts的组件元素,确定Timed SyncCharts的宏步转移机制;然后,提出将Timed SyncCharts转化为Kripke结构的规则,保证了模型分析的可行性;最后,建立计算机联锁软件道岔定位需求的Timed SyncCharts模型,证明该方法的可行性和有效性。

Focusing on the problems that the traditional complex modeling methods fail to satisfy the clock con-straint requirement of safety critical software for railway signal system,based on the analysis of the SyncCharts modeling method and in response to its lack of formal description and clock constraint,a modeling method of Timed SyncCharts with clock attributes was presented.First,the formal definition of Timed SyncCharts was proposed systematically with Z notion.Next,combined with the component elements of Timed SyncCharts, the Macro-step transfer mechanism was presented.Then,a rule which transformed Timed SyncCharts into Kripke structure was presented for model analysis.Finally,the Timed SyncCharts model of normal switch po-sition requirements of computer based interlocking was established,showing the feasibility and effectiveness of this method.