RBML: A Refined Behavior Modeling Language for Safety-Critical Hybrid Systems

As a widely used modeling language, AADL (Architecture Analysis and Design Language) plays an important role in designing safety-critical systems. It provides abundant components for describing system architecture and supports the early prediction and repetitive analysis of performance-critical attributes. However, the approach used by AADL to describe the system behavior is based mainly on automata theory; thus, encountering the state space explosion problem when modeling and verifying large and complex systems is inevitable. Furthermore, due to the lack of means to describe the behavior details, it is also difficult for AADL to support the accurate analysis and verification of functional and non-functional requirements. In this paper, we propose a language called RBML that supports refined behavior modeling to compensate for the behavior modeling and verification deficiencies of AADL. This new language is based on AADL but extends the ability to detail various behaviors and allows SMT (Satisfiability Modulo Theories) solvers to verify the constructed refined behavior model, thus alleviating the state space explosion problem to some extent. Experiments on Baidu Apollo are presented to demonstrate the feasibility of our proposed approach.