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

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