Title :
Extending EAST-ADL towards formal modeling and analysis of energy-aware real-time systems
Author :
Eun-Young Kang ; Schobbens, Pierre-Yves
Author_Institution :
PReCISE Res. Centre, Univ. of Namur, Namur, Belgium
Abstract :
Energy-aware Real-Time (ERT) systems are increasingly complex and have pervaded various areas, from automotive to telecommunication systems. EAST-ADL, an automotive specific architectural description language dedicated to safety-critical embedded control systems, has been proposed to harness this complexity. However, the current concept of EAST-ADL provides limited support for modeling and analysis of ERT behaviors due to the absence of energy constraints modeling notations and the lack of formal semantics. In this paper, we tackle that shortcoming by extending EAST-ADL notation with energy constraints and integrating the extension with formal analysis techniques based on ERT constraints. A mapping strategy is proposed to facilitate the guarantee of integration. The analysis techniques including the mapping strategy are validated and demonstrated on the Brake-By-Wire case study.
Keywords :
embedded systems; formal specification; formal verification; hardware description languages; power aware computing; EAST-ADL; ERT constraints; automotive specific architectural description language; automotive systems; brake-by-wire case study; electronics architecture and software technology; energy constraint modeling notations; energy-aware real-time systems; formal analysis techniques; formal semantics; mapping strategy; safety-critical embedded control systems; telecommunication systems; Analytical models; Clocks; Ports (Computers); Semantics; Synchronization; Unified modeling language; EAST-ADL; energy-aware real-timed systems; formal methods; model checking; timed-automata; validation; verification;
Conference_Titel :
Control and Automation (ICCA), 2013 10th IEEE International Conference on
Conference_Location :
Hangzhou
Print_ISBN :
978-1-4673-4707-5
DOI :
10.1109/ICCA.2013.6564929