CTCS-1级列控系统是为提升200km/h以下新建及改造线路安全性、可靠性、运输效率和自动化水平而对既有线列控系统进行的一次技术升级。列控系统作为典型的安全苛求系统,其安全性对整个铁路运输系统举足轻重,因此,对列控系统进行安全分析来识别特定应用场景存在的安全隐患,有着非常重要的意义。与传统的风险识别方法相比,STPA能够更系统地识别风险。但是STPA分析过程过度依靠人工,对技术人员的专家经验依赖程度高。另外由于复杂系统功能和行为的多样性,仅仅依靠人工分析难以保证结果的全面性和准确性。因此,本文基于CPN动态模型提出形式化的STPA-CPN方法来辨识系统危险致因。本文的主要研究工作如下:(1)首先,以侧线接车和临时限速场景为例,完成了 STPA的安全分析流程。在使用分层控制框图、SysML顺序图、OCL语言建立系统模型的基础上,参照STPA提供的四类引导词实现不恰当控制行为辨识,并完成控制缺陷分析,为验证本文所提方法有效性做铺垫。(2)然后,通过比较SysML和CPN两种建模方法的优缺点论证了 SysML活动图到有色Petri网模型转换的必要性和可操作性。建立侧线接车和临时限速两个场景的SysML活动图,给出活动图到CPN模型的转换规则及其简化规则,完成CPN模型的建立与化简。并运用CPN Tools工具生成两个场景CPN模型的状态空间可达图。(3)为提高本文提出的形式化安全分析方法的通用性,在编写搜索危险状态可达路径程序的基础上,于C#环境下完成了可达性分析工具Reachability Analysis Tool的开发。该工具以不安全控制行为和状态空间可达图为输入,输出为危险状态可达路径。(4)最后,根据可达性分析工具输出的危险状态可达路径,通过追溯状态迁移过程进行致因分析,改善了 STPA中依靠人工辨识容易出现遗漏和错误的问题,并且降低了对安全分析人员专家经验的依赖。并与STPA安全分析出的结果对比,结果证明将CPN可达性分析引入STPA是可行、有效的。图62幅,表5个,参考文献72篇