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

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

作　　者：李腾飞 孙军峰 吕新军 陈祥 刘静[2] 孙海英[2] 何积丰[2] LI Teng-Fei;SUN Jun-Feng;LÜXin-Jun;CHEN Xiang;LIU Jing;SUN Hai-Ying;HE Ji-Feng(CASCO Signal Ltd.,Shanghai 200072,China;Software Engineering Institute,East China Normal University,Shanghai 200062,China)

机构地区：[1]卡斯柯信号有限公司,上海200072 [2]华东师范大学软件工程学院,上海200062

出　　处：《软件学报》2023年第7期3080-3098,共19页Journal of Software

基　　金：国家重点研发计划(2019YFA0706404);国家自然科学基金(61972150);上海市超级博士后基金(2021146)。

摘　　要：在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.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 verification of the software model in implementation level.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.Thus,it is drawn on the insight that the synchronous reactive model of safety-critical systems should be verified completely,and the data-flow models should be considered.An approach is presented for automated,generic verification that tailor to verify the integration of safe state machines and data-flow models.Furthermore,a synthesis-based approach is adopted 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.The proposed technique promotes program synthesis as a general primitive for improving the integrity of formal verification.The proposed approach is evaluated on an industrial application(nearly two million lines of Lustre code)in rail transit.It is show that the proposed approach is effective in sidestepping long-standing and complex verification issues in large scale synchronous reactive model.

关 键 词：形式化验证 安全关键系统 同步反应式模型 高阶迭代 程序转换 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]