An SMT-based Approach To Formal Analysis Of MARTE/CCSL And Its Applications

With the increasing complexity and security of real-time embedded systems in areas such as automotive and avionics,it is important to apply rigorous analysis techniques to ensure system predictability.Therefore,the Unified Modeling Language(UML)adopts MARTE(Modeling and Analysis of Real-Time and Embedded Systems)as an extension of its real-time embedded system,which provides support for specification,design,and verification/validation stages.MARTE provides a rich time model.When using the MARTE time model,many mutually dependent clocks are defined in the model.This dependency can be specified by a dedicated language,which is called the Clock Constraint Specification Language(CCSL).CCSL specifies the constrained relationships between clocks that are synchronous and asynchronous,providing support for causal timing analysis on the MARTE model.An important issue is to verify the satisfiability of CCSL constraints that describe the timing requirements of the system models.This problem can help developers find defects during the system design phase,thereby avoiding unnecessary losses during the development phase.At present,many researchers are exploring approaches to the formal analysis of CCSL,mainly using the transition systems,Promela,Büchi automata,timed automata,Rewrite Logic,etc.to encode the CCSL constraints and combining with the corresponding tools for analysis and verification.However,some methods require an unusual intermediate encoding process that can easily lead to errors or inefficiency.Some encoding methods cannot encode all constraints or only consider partial constraints.State-based methods can easily lead to state explosions,affecting the efficiency of the analysis.This thesis proposes a unified and efficient method to formal analysis of CCSL based on SMT,which can be used for schedulability analysis,LTL model checking,deadlock detection,entailment proving and trace analysis of CCSL,with the efficient SMT solver Z3 and CVC4 for analysis and verification.The process of encoding CCSL constraints into SMT formulas is very natural,avoiding complicated intermediate encoding processes,thereby reducing the risk of errors.Unlike some methods that can only encode partial CCSL constraints,the encoding of CCSL constraints to SMT formulas does not have this limitation.As we all know,the method based on SMT can effectively overcome the stateexplosion problem in model checking.This method improves the efficiency of model checking of CCSL constraints.At the same time,the SMT-based method can also be used to prove properties of CCSL constraints by means of theorem proving,which is the lack of most of the existing CCSL formal analysis methods.This thesis not only explains the theoretical implementation of the SMT-based approach to formal analysis of CCSL in five aspects,but also gives corresponding practical examples to demonstrate the feasibility and effectiveness of the method.An analysis and verification tool for CCSL integrated the proposed approach is independently developed and a case of a railway interlocking system is applied.