基于SMT的区域控制器同步反应式模型的形式化验证

在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.

SMT-based Formal Verification of Synchronous Reactive Model for Zone Controller

Formal verification is a proven technique for improving product quality during software development of safety critical systems.However, the verification must be complete, both theoretically and in the interest of practicality.Data-flow verification is a pervading manifestation of such verification approaches-environmental input, generic function, high order iterative operation and intermediate variables are therefore crucial for analyzing usability of verification approaches.To verify a synchronous reactive model, engineers readily verify the control-flow model (i.e., safe state machine).Existing work shows that these approaches fall short of complete verification of synchronous reactive model of industrial software, which results in the loss of reaching the industrial requirements. It presents a significant pain point for adopting formal verification of industrial software.We draw on the insight that the synchronous reactive model of safety-critical systems should be verified completely, and the data-flow models should be considered.We present a novel approach for automated, generic verification that tailor to verify the integration of safe state machines and data-flow models.Furthermore, we adopt a synthesis-based approach where the SCADE models describe functional requirements, safety requirements and environmental inputs that can be verified for an SMT-based model checker through program synthesis to Lustre model.Our technique promotes program synthesis as a general primitive for improving the integrity of formal verification.We evaluate our approach on an industrial application (nearly two million line Lustre code) in rail transit.We show that our approach is effective in sidestepping long-standing and complex verification issues in large scale synchronous reactive model.