Logotype Mälardalenn University

MRTC publications



A Formal Analysis Framework for AADL

Full text:  
Authors: Stefan Björnander, Cristina Seceleanu, Kristina Lundqvist, Paul Pettersson
Source: The Journal of Science and Technology
 

Abstract

As system failure of mission-critical embedded systems may result in serious consequences, the development process should include verification techniques already at the architectural design stage, in order to provide evidence that the architecture fulfils its requirements. The Architecture Analysis and Design Language (AADL) is a language designed for modeling embedded systems, and its Behavior Annex defines the behavior of the system. However, even though it is an internationally used industry standard, AADL still lacks a formal semantics and is not executable, which limits the possibility to perform formal verification. In this paper, we introduce a formal analysis framework for a subset of AADL and its Behavior Annex, which includes the following: a denotational semantics, its implementation in Standard ML, and a graphical Eclipse-based tool encapsulating the implementation. We also show how to perform model checking of AADL properties defined in the Computation Tree Logic (CTL).
 

BibTeX entry

@article{Björnander_2729:2011,
   author = {Stefan Bj{\"o}rnander and Cristina Seceleanu and Kristina Lundqvist and Paul Pettersson},
   title = {A Formal Analysis Framework for AADL},
   journal = {The Journal of Science and Technology},
   month = {November},
   year = {2011},
   url = {http://www.mrtc.mdh.se/index.php?choice=publications&id=2729},
}

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2012.08.24