安全苛求控制系统是一类对可靠性和安全性要求极高的系统,其正常运行依赖于正确的功能控制逻辑和配置数据。这样的配置数据称为安全苛求数据,这样的功能控制逻辑包含各个安全苛求功能场景。因而使用有效的方法保证安全苛求数据及功能场景的正确性显得十分重要。通过使用形式化方法来发现系统的数据及功能场景存在的错误和缺陷,进而完善系统设计,达到增强系统可靠性和安全性的目的。论文主要研究内容如下:（1）以安全苛求数据为研究对象,选取道岔、信号机、轨道区段、进路等铁路信号设备数据为研究案例,基于各个安全苛求数据的数据结构,先用自然语言描述各个安全苛求数据需要满足的静态规则,而后使用Atelier B工具建立数据所需要满足的静态规则的形式化模型,最后使用ProB模型检验工具,结合Graphviz可视化图形软件,验证分析已生成的各个安全苛求数据是否满足静态规则。在研究过程中,考虑到已生成的数据量庞大,使用支持Z语言格式转换的Epsilon脚本语言,实现了将形式定义后的数据自动导入至B模型文件。（2）以安全苛求功能场景为研究对象,选取具有安全风险特征的平交道口控制系统功能逻辑流程为研究案例,分析功能设计规范,析取得到各个基本功能场景和安全场景,先使用Simulink/Stateflow工具建模得到各个基本功能场景的半形式化模型,而后使用AterlierB工具建模得到各个基本功能场景的形式化模型,并用不变式描述安全属性,利用ProB模型检验工具检查功能模型是否满足不变式,结合AtelierB内建的交互式证明平台,完成对生成的证明义务的交互式证明。将上述半形式化模型和形式化模型生成可执行代码。基于各个基本功能场景和形式化验证过程中发现的缺陷,应用软件测试方法中的场景法和错误估计法,编写测试用例,使用BTC Embedded System商业测试验证平台,对生成的代码进行测试,测试结果表明,所建立的半形式化模型实现了各个基本功能,但存在违反安全属性的显性缺陷和建模不完善的隐性缺陷,所建立的形式化模型存在一个基本功能没有实现。基于测试结果,从一定程度上反映了半形式化建模方法更可能构建出具有较高实用性的模型,形式化建模方法更可能构建出具有较高安全性的模型。论文实现了安全苛求数据及功能场景的建模验证及测试,对系统建模开发过程中如何提升数据的正确性、模型的可靠性、安全性,提供了参考借鉴的意义。