铁路信号系统是指挥和控制高速列车安全运行,提高区间和车站的通过能力的关键系统。随着计算机和信息技术的发展,铁路信号系统中的许多控制逻辑已逐渐转变为软件逻辑,越来越多的安全关键功能也逐渐由软件实现,安全关键软件已经成为铁路信号系统的重要组成部分。随着铁路信号系统的结构越来越复杂,自动化程度越来越高,铁路信号系统安全关键软件的规模也越来越大,逻辑也越来越复杂,软件失效轻则造成运行中断,影响行车效率,重则可能发生追尾和出轨等安全事故,造成重大人员伤亡和财产损失。因此,铁路信号系统安全关键软件的正确性和安全性必须得到严格的分析和验证,将风险控制在可接受的范围内。形式化建模和分析是验证软件逻辑的正确性和安全性、指导软件设计和开发、分析软件风险的重要方法,EN 50128强烈推荐对SIL 3和SIL 4等级的铁路信号系统安全关键软件采用形式化方法。目前比较成熟的形式化建模和分析方法包括时间自动机、UML Statecharts和Petri网等理论,已经广泛应用于软件建模与分析领域,但由于铁路信号安全关键软件逻辑复杂,对实时性和安全性要求高等特点,目前的建模和分析方法不能完整地描述铁路信号系统安全关键软件的功能逻辑、时钟约束和风险特征,导致软件安全性分析、需求分析、软件设计和软件测试等活动过程中,软件人员根据各自关注的方面,独立地选择形式化建模和分析方法,单独建立各个阶段的形式化模型。由于没有系统化地描述软件的功能逻辑、时钟约束和风险,容易造成模型之间描述不一致,不同阶段的人员彼此不理解对方模型等问题,为软件留下安全隐患。因此,一种能够全面地描述功能逻辑、时钟约束和风险的形式化建模和分析方法对我国铁路信号系统安全关键软件的发展具有一定的理论和现实意义。本文以提出统一铁路信号系统安全关键软件功能逻辑、时钟约束和风险特征的形式化建模和分析方法为目标,主要进行了以下几方面的研究:(1)针对铁路信号系统安全关键软件对形式化建模和分析方法的需求,根据SyncCharts建模方法具有层次性、并发性和优先级抢占机制等特点,选取SyncCharts建模理论作为研究对象,研究铁路信号系统安全关键软件的形式化建模和分析方法。(2)针对SyncCharts缺乏描述时钟约束的缺陷,在SyncCharts建模理论中引入时钟属性,提出时间SyncCharts建模方法,采用Z规格说明语言描述时间SyncCharts的基本元素、层次结构等语法和语义,满足铁路信号系统安全关键软件对功能逻辑和时钟约束的建模需求。(3)针对铁路信号系统对风险的建模需求,在时间SyncCharts的基础上引入频数和失效后果严重度两个属性,分别描述软件功能之间的转移频率和软件功能失效后对系统造成的后果严重度等级,提出风险时间SyncCharts建模方法描述软件功能失效后的风险特性,给出风险时间SyncCharts的定义、宏步转移机制和元模型,满足铁路信号系统安全关键软件对功能逻辑、时钟约束和风险的建模需求。(4)针对风险时间SyncCharts的模型检测,提出将风险时间SyncCharts转换为UTA的方法,通过UTA的模型检测算法实现风险时间SyncCharts的模型检测,完成风险时间SyncCharts功能逻辑和时钟约束的分析;提出将风险时间SyncCharts转换为MDP的方法,通过MDP的概率模型检测算法实现风险时间SyncCharts的概率模型检测,完成风险时间SyncCharts概率和风险特性的分析。(5)以计算机联锁道岔模块安全关键软件为例,利用风险时间SyncCharts对软件的功能逻辑、时钟约束和风险特性进行建模,然后将道岔模块的风险时间SyncCharts模型转换为UTA和MDP模型,分别利用UTA和MDP的模型检测和概率模型检测方法分析风险时间SyncCharts模型的功能逻辑、时钟约束和风险特征,验证风险时间SyncCharts在铁路信号系统安全关键软件形式化建模和分析中的可行性。