形式化验证在轨道交通领域的应用

摘要

随着轨道交通跨越式发展,越来越多的现代科技、国防和国民经济领域依赖轨道交通.轨道交通的安全性和可靠性成为国家和人民关注的重点.由于轨道交通领域的特殊性,传统的模拟和测试方法不能保证软件和硬件的可靠性.形式化方法可以保证从软件需求到软件编码全过程的逻辑一致性.最近几年,工程和学术界广泛使用形式化验证来对软件进行建模.该文介绍了形式化验证在轨道交通领域的应用,这包括软件需求、设计的形式化描述和软件的形式化建模.