DocumentCode :
3641223
Title :
ABV - A Verifier for the Architecture Analysis and Design Language (AADL)
Author :
Stefan Björnander;Cristina Seceleanu;Kristina Lundqvist;Paul Pettersson
Author_Institution :
Sch. of Innovation, Design, &
fYear :
2011
fDate :
4/1/2011 12:00:00 AM
Firstpage :
355
Lastpage :
360
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.
Keywords :
"Computer architecture","Semantics","Production","Unified modeling language","Computational modeling","Embedded systems","Generators"
Publisher :
ieee
Conference_Titel :
Engineering of Complex Computer Systems (ICECCS), 2011 16th IEEE International Conference on
Print_ISBN :
978-1-61284-853-2
Type :
conf
DOI :
10.1109/ICECCS.2011.43
Filename :
5773410
Link To Document :
بازگشت