RBML:A Refined Behavior Modeling Language For Safety-critical Hybrid Systems

With the increase of functional requirements,the design of safety-critical systems becomes more and more complex.How to ensure the quality of safety-critical systems through modeling and verification has always been a concern in the field of formal methods.As a widely used modeling language,AADL plays an important role in the design and implementation of safety-critical systems.It provides a rich set of components to describe the architecture of the system and supports early prediction and repetitive analysis of performance-critical attributes.However,the way AADL describes system behavior is mainly based on automata theory,which inevitably encounters the problem of state space explosion when modeling and verifying large complex systems.In addition,due to the lack of means to describe the details of behavior,AADL is difficult to support the analysis and verification of functional requirements,which leads to the failure to ensure the correctness and safety of the whole system.Aiming at the shortcomings of the AADL language in behavior description and model verification,this paper proposes a refined behavior modeling method based on constraint solving.This method extends the AADL language to enhance its ability of describing behavioral details,and can support Z3 solver to analyze and verify the constructed refined behavior model,thus alleviating the situation of state space explosion to some extent.The main contributions of this paper are as follows:(1)Based on the extension mechanism of the AADL language,a sublanguage RBML which can support refined behavior modeling is proposed,and its syntax and semantics are given.The language innovatively introduces a custom mechanism to increase flexibility in behavioral modeling.It allows users to define variables,functions,and constraints in the RBML specification as needed to describe the data,behavior,and requirements that the AADL core language cannot express.(2)The transformation rules from the RBML language to Z3 solver are defined and the main transformation algorithms are designed.This paper chooses Z3 solver as the verification tool,which can effectively alleviate the problem of state space explosion while improving the efficiency of verification.This paper also uses OpenModelica to simulate continuous behavior in the RBML specifications to enhance the reliability of verification results.(3)A tool chain is designed and implemented to support the modeling,verification and simulation of the RBML language.This paper implements the integration of the RBML language on OSTAE platform,allowing users to insert RBML annex specifications into AADL models to support refined behavior modeling.In addition,a model transformation tool AADL2 ZAO is developed to automatically convert AADL models into corresponding formal specifications.The tool also builds the connections with Z3 and OpenModelica to verify and simulate the specifications generated by the transformation.This paper takes Baidu Apollo automatic driving system as an example to illustrate the specific application of the RBML language in behavior modeling and analysis of safety-critical systems.The experimental results show that the proposed approach can effectively model and analyze the implementation details of the behavior,thus ensuring the correctness of the functional design and the safety of the whole system.