Abstract |
This paper presents first steps towards a formalisation of the
Architecture Analysis and Design Language, mainly concentrating on a
representation of its data model. For this, we contrast two
approaches: one set-based (using the B modelling framework) and one in
a higher-order logic (using the Isabelle proof assistant). We
illustrate a transformation on a simplified part of the AADL metamodel
concerning flows.
Online Copy |
Available as PS
BibTeX Entry |
@InProceedings{ BoChFiSt2005, author = {Bodeveix, Jean-Paul and Chemouil, David and Filali, Mamoun and Strecker, Martin}, title = "{Towards formalizing AADL in proof assistants}", year = 2005, pages = {137--153}, editor = {Kuster-Filipe, Juliana and Poernomo , Iman and Reussner, Ralf and Shukla, Sandeep}, publisher = {LFCS (University of Edinburgh)}, booktitle = {Formal Foundations of Embedded software and component-based softare architectures (ETAPS), Edinburgh} }
Last modified: Thu Jul 30 10:56:52 CEST 2009 |