Model-based Verification and Validation of an Autonomous Vehicle System

The software development for Cyber-Physical Systems (CPS), e.g., autonomous vehicles, requires both functional and non-functional quality assurance to guarantee that the CPS operates safely and effectively. EAST-ADL is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time (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 and an integration of Simulink/Stateflow within a same tool-chain. Simulink/Stateflow models are transformed, based on extended ERT constraints in EAST-ADL, into verifiable UPPAAL models with stochastic semantics and integrate the translation with formal statistical analysis techniques: Probabilistic extension of EAST-ADL constraints is defined as a semantics denotation. A set of mapping rules is proposed to facilitate the guarantee of translation. Formal analysis on both functional- and non-functional properties is performed using SIMULINK DESIGN VERIFIER/UPPAAL-SMC. The analysis techniques are validated and demonstrated on the autonomous traffic sign recognition vehicle case study.