论文以道岔状态监测单元作为研究对象,针对智能化情景下的铁路系统安全决策问题,使用形式化开发方法严格的定义了该系统软件的逻辑决策层,完成了系统原型机的构建与软件决策进程的验证,增强了系统的可信性。基于安全苛求系统的特征构建系统硬件架构,基于系统的可验证性要求,设计系统软件架构。在系统软件架构中将控制流与数据流分离,作为系统软件的逻辑决策层和形式化建模和验证的对象。并结合实际应用场景提出保障系统可靠性的措施;使用工具链建立从半形式化到形式化的建模验证方案。针对系统软件的逻辑决策层,借助基于系统理论的事故模型过程分析方法(STAMP)的危险致因分析来发现当前系统的缺陷并反推系统的安全约束,并根据实际的应用场景完善功能需求,结合软件决策层的层次结构建立需求元模型。根据需求元模型确定参数类型和程序框架,建立数据字典,并一步实例化元模型中的功能,建立程序流程图。最终将数据参数与程序流程图模型化为Simulink的Stateflow模型,为形式化建模提供实现的模板和仿真依据;形式化建模和验证阶段根据系统软件逻辑决策层纯布尔逻辑的特性定制B方法的建模和验证方案,使之更简单、高效,且有针对性;根据元模型和Simulink的Stateflow模型形式化建模,并使用安全约束构建的不变式和Pro B的模型检测功能证明模型的正确性,最终生成目标代码。最后,添加并集成具体的实现算法、构建联锁环境,在仿真环境中进一步测试和确认系统的功能满足性。论文中实现了道岔状态监测单元软件逻辑决策层的形式化开发。该安全关键模块的逻辑模型在Atelier B平台中被证明通过,并可生成相应的嵌入式代码,将代码集成并在仿真环境中完成了仿真。课题的整个技术过程证明了课题中设计的开发路线适用于定义和开发此类复杂逻辑系统,可为安全苛求系统的开发提供参考。