| As one of the important measures to guarantee that software systems meet the design of requirement,model checking has received increasing attention in the design and development of modern systems,especially in reactive real-time systems.In the field of reactive real-time systems,Lustre synchronous dataflow language occupies a representative position.With the wide-spreading use of Lustre language in aerospace,industrial energy and rail transportation,the strict requirement for software correctness in these fields makes it critical to verify the programs written in Lustre.There are already many tools for verifying Lustre programs,which have been used in the industrial field to some extent.However,these tools focus almost exclusively on safety properties,and currently there are no tools available to support the verification of liveness properties.In order to fill this gap,this paper proposes a formal semantics for Lustre language which is suitable for verification,then designs and implements a model checker supporting both safety and liveness properties,which is based on SMT solvers.The main research work of this paper is listed as follows:· Proposes a formal semantics of Lustre language: In order to convert Lustre models into transition systems,this paper explains in detail the meaning of each syntax structure,including nodes and expressions.Then it proposes an formal semantics according to Lustre language.The properties at a specific moment and overall time are described respectively from two perspective,instantaneous semantics and dataflow semantics,which ensures the correctness of model transformation in the subsequent model checking process in theory.· Designs and implements a Lustre model checker supporting safety and liveness properties: After parsing the Lustre program,the verification process is separated in to three parts: Lustre simplifier for eliminating complex structure,SMT translator for converting Lustre program into transition system and verification controller for verifying the properties.Algorithms including BMC,kinduction,invariant generation and IC3 are use for verification in parallel.Meanwhile,L2SIA-WFR is integrated to provide support for liveness properties.· Evaluates and analyzes the model checker with safety and liveness benchmarks: The implemented model checker,NKind,is evaluated and analyzed with classic benchmarks in both safety and liveness properties,and the performance is compared to existing tools like Kind2,JKind and ic3 ia.The result of the evaluation shows that NKind is able to solve safety and liveness properties effectively and has a competitive performance comparing to existing tools. |
