| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Analysis Support for TADL2 Timing Constraints on EAST-ADL Models
Abstract : It is critical to analyze characteristics of real-time embedded systems, such as timing behavior, early in the development. In the automotive domain, EAST-ADL is a concrete example of the model-based approach for the architectural modeling of real-time systems. The Timing Augmented Description Language v2 (TADL2) allows for the specification of timing constraints on top of EAST-ADL models. In this paper we propose a formal validation & verification methodology for timing behaviors given with TADL2. The formal semantics of the timing constraints is given as a mapping to the Clock Constraint Specification Language (CCSL), a formal language that implements the MARTE Time Model. Based on such a mapping, the validation is carried out by the simulation of TADL2 specifications. The simulation allows for a rapid prototyping of TADL2 specifications. The verification is performed based on a TADL2 mapping to timed automata modeling using the UPPAAL model-checker. The whole process is illustrated on a Brake-By-Wire application.
https://hal.inria.fr/hal-00839963
Contributor : Frédéric Mallet Connect in order to contact the contributor
Submitted on : Monday, July 1, 2013 - 11:44:54 AM
Last modification on : Tuesday, January 11, 2022 - 11:16:22 AM
Contributor : Frédéric Mallet Connect in order to contact the contributor
Submitted on : Monday, July 1, 2013 - 11:44:54 AM
Last modification on : Tuesday, January 11, 2022 - 11:16:22 AM
Links full text
