Towards formalising AADL in Proof Assistants

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}
}