Logotype Mälardalenn University

PROGRESS publications



ABV – A Verifier for the Architecture Analysis and Design Language (AADL)

Full text:  
Authors: Stefan Björnander, Cristina Seceleanu, Kristina Lundqvist, Paul Pettersson
Source: Sixth IEEE International Workshop UML and AADL at ICECCS 2011
 

Abstract

Designing and developing mission-critical embedded systems is challenging, especially due to additional platform constraints regarding timing and computational resources. The development process of embedded systems should include verification techniques already at the architecture design phase, to provide evidence that a system's architecture fulfills its requirements. The Architecture Analysis and Design Language (AADL) is used to model the system's architecture. Among others, the language contains a Behavior Annex, for describing the behavior of an AADL model, at an abstract level. In this paper, we present a verification tool, called ABV, tailored for AADL models with a behavioral annex. Given an architecture defined in AADL and its behavior specified in the associated language, our tool model-checks the latter against the requirements specified in Computation Tree Logic (CTL). ABV is based on AADL's formal denotational semantics implemented in Standard ML, and is encapsulated into an Eclipse plug-in based on the OSATE platform. The tool has been applied on the Production Cell case study, which is briefly described in the paper.
 

BibTeX entry

@inproceedings{Björnander_2406:2011,
   author = {Stefan Bj{\"o}rnander and Cristina Seceleanu and Kristina Lundqvist and Paul Pettersson},
   title = {ABV – A Verifier for the Architecture Analysis and Design Language (AADL)},
   booktitle = {Sixth IEEE International Workshop UML and AADL at ICECCS 2011 },
   month = {April},
   year = {2011},
   url = {http://www.mrtc.mdh.se/index.php?choice=publications&id=2406},
}

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