2018/03/16 by Eun-Young Kang, Dongrui Mu, Kang, Eun-Young +5
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Real-Time Systems Scheduling #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.1803.06103
openalex publication_date 2018/03/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.