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

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.