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

Automated Verification of AADL-Specifications Using UPPAAL

Fulltext:


Authors:

Andreas Johnsen, Kristina Lundqvist, Paul Pettersson, Omar Jaradat

Research group:

Safety-Critical Engineering

Publication Type:

Conference/Workshop Paper

Venue:

14th IEEE International Symposium on High Assurance Systems Engineering

Publisher:

IEEE

Abstract

The Architecture Analysis and Design Language (AADL) is used to represent architecture design decisions of safety-critical and real-time embedded systems. Due to the far-reaching effects these decisions have on the development process, an architecture design fault is likely to have a significant deteriorating impact through the complete process. Automated fault avoidance of architecture design decisions therefore has the potential to significantly reduce the cost of the development while increasing the dependability of the end product. To provide means for automated fault avoidance when developing systems specified in AADL, a formal verification technique has been developed to ensure completeness and consistency of an AADL specification as well as its conformity with the end product. The approach requires the semantics of AADL to be formalized and implemented. We use the methodology of semantic anchoring to contribute with a formal and implemented semantics of a subset of AADL through a set of transformation rules to timed automata constructs. In addition, the verification technique, including the transformation rules, is validated using a case study of a safety-critical fuel-level system developed by a major vehicle manufacturer.

Bibtex

@inproceedings{Johnsen2630,
author = {Andreas Johnsen and Kristina Lundqvist and Paul Pettersson and Omar Jaradat},
title = {Automated Verification of AADL-Specifications Using UPPAAL},
pages = {130--138},
month = {October},
year = {2012},
booktitle = {Proceedings of the 14th IEEE International Symposium on High Assurance Systems Engineering (HASE)},
publisher = {IEEE},
url = {http://www.es.mdu.se/publications/2630-}
}