Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:
Academic
Publications
ABV - A Verifier for the Architecture Analysis and Design Language (AADL)
Edit
ABV - A Verifier for the Architecture Analysis and Design Language (AADL)  
BibTex | RIS | RefWorks Download
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 veri- fication techniques already at the architecture design phase, to provide evidence that a system's architecture fulfills its require- ments. 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. Index Terms—Model Checking, Verification, AADL, Behavior Annex, CTL, OSATE, Denotational Semantics.
Conference: International Conference on Engineering of Complex Computer Systems - ICECCS , 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Share this on | Contribute to Academic