反应堆保护系统是核电厂最重要的仪控系统之一,当和反应堆运行状态相关的参数达到极限值时触发紧急停堆和安全专设系统,确保核电站的安全运行。反应堆保护系统安全软件失效时可能造成事件乃至重大核泄漏事故,因此软件必须具备极高的可靠性和安全性,传统软件的手工代码开发模式,工作量巨大,且容易出错,难以满足核电安全软件的高可靠性要求。目前国外也有通过PLC梯形图搭建逻辑,再手工翻译成C代码的开发方法,虽然同时开展V&V工作对软件进行验证与确认,但其仍然不能彻底满足软件安全性需求。形式化建模是关键安全系统软件开发的重要方法之一。法国艾斯特尔公司开发的高安全性应用开发环境SCADE提供了一种基于模型的形式化建模方法,其具有严格的数学理论基础,能实现对系统功能需求的清晰、无歧义表达,相比传统手工编码开发,大大降低了代码出现模糊性和二义性问题的概率,并能够实现需求的逻辑追溯。SCADE为高安全性软件开发人员提供了数据流和安全状态机两种开发方法,能够完整的实现软件功能逻辑,同时提供模型验证方法,大大提高了模型的正确性和安全性,模型验证后还能生成认证级的高质量C代码,提供了高可靠性关键安全软件开发的完整流程。美中不足的是SCADE工具没有时间概念,对于实际存的在时序和延时问题没有针对性的验证。本文研究基于SCADE的反应堆保护系统RTS软件开发方法,在分布式RPR系统的研究基础上,利用SCADE的数据流建模、静态检查、功能测试、覆盖率分析、形式化验证以及代码生成工具等功能对分布式RPR停堆逻辑软件进行了开发。研究了 SCADE缺陷的基础上,本文提出了针对分布式RPR系统的停堆模型同步性和确定性验证方法,引入simulink工具进行了分布式RPR系统同步性验证。主要工作如下:(1)根据核反应堆保护系统发展现状和未来趋势,介绍了三代反应堆保护系统结构、功能及特点,同时对核电安全软件开发的V&V过程进行了简述,确定了模型开发路线,重点分析了停堆逻辑,确定了软件建模需求。(2)阐述SCADE工具的确定性与同步性机理。介绍了分布式RPR系统的确定性与同步性需求,说明了 SCADE对于分布式RPR系统同步性设计上的不足,通过SCADE用数据流建模方法对核反应堆RPR系统停堆逻辑进行建模并把各个子模型进行了系统集成。(3)模型确定性验证,采用SCADE工具通过手工编写测试用例进行覆盖率分析、形式化验证等方式验证了模型与需求的一致性。分布式RPR系统的同步性验证主要是引入simulink工具,在输入端加入延时,进行对比测试,最后验证了模型的同步性。(4)通过SCADE KCG组件,对所建模型生成了认证级C代码,简述了SCADE生成代码的特点,并将代码移植到VS上简单运行测试,证明了在保持高安全性要求下SCADE代码的可用性。