Model-Based Analysis of Timing and Energy Constraints in an Autonomous Vehicle System
Eun-Young Kang, Dongrui Mu, Li Huang, Qianqing Lan · 2017
Modeling and analysis of non-functional properties is crucial in energy-aware real-time (ERT) automotive systems. EAST-ADL is an architectural language dedicated to safety critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed ERT behaviors modeled in EAST-ADL/STATEFLOW into UPPAAL models amenable to formal verification. Previous work is extended in this paper by including support for SIMULINK. Furthermore, probabilistic extension of EAST-ADL constraints is defined and the semantics of the extended constraints is translated into verifiable UPPAAL models with stochastic semantics for the formal verification: A set of mapping rules is proposed to facilitate the guarantee of translation. Simulation and Verification & Validation are performed on the extended timing and energy constraints using UPPAAL-SMC and SIMULINK. Our approach is demonstrated on the autonomous traffic sign recognition vehicle case study.