Model-Based Verification of Energy-Aware Real-Time Automotive Systems

EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design with a focus on structural specification and behavioral constraints. The current concept of EAST-ADL provides limited support for modeling and analysis of Energy-aware Real-Time (ERT) behaviors due to the absence of energy constraints modeling notations and the lack of formal semantics. We address these limitations by extending the EAST-ADL notation with energy constraints and integrating this extension with formal modeling and analysis techniques. We provide a mapping scheme as the basis for automatic model transformation between the extended EAST-ADL and priced timed automata for model checking. This methodology has been implemented in a tool called A-BeTA and is demonstrated by means of the Brake-By-Wire case study. Our approach enables formal modeling and verification of ERT systems in EAST-ADL and identifies potential conflicts between different automotive functions at an early stage of development.