基于PVS对SCADE开发轨交控制系统的形式化建模与验证

摘要

随着计算机微处理器技术的迅速发展，嵌入式系统的设计越来越复杂。特别是对于安全性要求极高的系统，例如飞机，火箭，轨道列车控制系统等等。设计中的任何细小的缺陷都有可能造成灾难性后果，并造成巨大的经济损失。因此，研究如何设计出高可信的嵌入式系统是非常重要的。
　　 轨交控制系统对可靠性要求是非常高的，单单传统的验证方法已经不能满足要求，需要提出新的建模与验证方法来完成其开发设计。为此本文提出了一种基于PVS(原型验证系统)对SCADE开发轨交控制系统的形式化建模与验证的方法。研究以SCADE Suite作为开发工具的图形化建模方式和由SCADE Suite生成的图形模型自动转换的Lustre语言。在此基础上，对于基本Lustre语言，包括constants常量、variable变量、condition条件语句、special operator特殊操作符等给出在PVS中的转换规则，对于扩展Lustre语言状态描述的部分，则给出了对其转换的基本策略。在SCADE Suite建立模型的基础上，根据SCADE转换至PVS的规则，逐行读取建模后所生成的代码，并将之转换成PVS的相应理论，通过Ruby脚本语言，设计并实现了由Lustre语言到PVS转换工具，SCADE2PVS。在SCADE Suite建立模型的基础上，根据SCADE转换至PVS的规则，逐行读取建模后所生成的每一行代码，并将之转换成PVS的相应理论。
　　 最后通过轨道交通控制系统中的列车道岔换轨例子说明了该方法的可行性，阐述了通过SCADE2PVS工具，把在SCADE Suite中的建立的模型转换成PVS理论的方法，并在形成的PVS理论中证明了列车道岔的性质。