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

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