嵌入式控制系统时序安全性建模及验证

摘要

针对嵌入式控制系统中的时序安全问题,提出一种形式化验证方法,使用证明助手Coq对嵌入式控制系统建模,并验证其时序安全性质。首先,将控制系统的运行过程描述为基于状态转移图的自动机中间模型,并建立转移关系语义公式,提高模型与系统的一致性;其次,使用线性时序逻辑将自然语言表达的安全约束转换为时序逻辑公式,消除自然语言表达的二义性;最后,在Coq中实现系统的形式化模型,将约束公式转换为Coq中的定理,并选择合适的策略进行证明。使用该方法对C语言编写的直角坐标型机器人控制系统进行建模,实验结果表明,模型满足文中设计提出的若干性质,发现程序中隐藏的时序安全问题并对其进行了有效修复。