You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact webmaster@ide.mdh.se

Analysis Support for TADL2 Timing Constraints on EAST-ADL Models

Fulltext:


Authors:

Arda Goknil , Jagadish Suryadevara, Marie-Agnes Peraldi-Frati , Frederic Mallet

Research group:

Formal Modelling and Analysis of Embedded Systems

Publication Type:

Conference/Workshop Paper

Venue:

7th European Conference on Software Architecture (ECSA)

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 v.2 (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 considered 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 through a mapping to Timed Automata implemented by UPPAAL. The whole process is illustrated on a Brake-By-Wire application.

Bibtex

@inproceedings{Goknil2790,
author = {Arda Goknil and Jagadish Suryadevara and Marie-Agnes Peraldi-Frati and Frederic Mallet},
title = {Analysis Support for TADL2 Timing Constraints on EAST-ADL Models},
month = {July},
year = {2013},
booktitle = {7th European Conference on Software Architecture (ECSA)},
url = {http://www.es.mdu.se/publications/2790-}
}