  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.
