Towards the Integration of EAST-ADL and UPPAAL for FormalVerification of EAST-ADL Timing Constraint Specification
2011 (English)Conference paper (Refereed)
EAST-ADL is an architecture description language developed for specifications of automotive embedded systems at multiple abstraction levels. Based on the best practices in model-based system development (MBD), it provides necessary artifacts for integrating and managing various concerns in an entire system lifecycle. Requirements engineering, safety engineering and the assignments of nonfunctional constraints are few examples of the concerns supported by EAST-ADL. This paper presents an effort to investigate the support for a formal verification of the execution timing constraints declared in EAST-ADL using the UPPAAL model checker. The results include a transformation scheme and a prototype transformation employing MQL (Model Query Language). Two case studies, of an emergency braking system and a brake-by-wire system, are used to support the work.
Place, publisher, year, edition, pages
Model-based development, timing analysis, EAST-ADL, UPPAAL, model transformation, MDWorkbench, MQL, timed automata, formal methods, model checking.
Embedded Systems Computer Systems
IdentifiersURN: urn:nbn:se:kth:diva-79675OAI: oai:DiVA.org:kth-79675DiVA: diva2:495691
Time Analysis and Model-Based Design, from Functional Models to Distributed Deployments
FunderEU, FP7, Seventh Framework Programme, 260057
Qc 201202142012-02-142012-02-092012-10-22Bibliographically approved