Open AccessTowards Formal Specification for AADL with Behavior Annex in Isabelle
Author(s) -
Yu Tan,
Dianfu Ma,
Lei Qiao
Publication year - 2021
Publication title -
iop conference series. earth and environmental science
Language(s) - English
Resource type - Journals
eISSN - 1755-1307
pISSN - 1755-1315
DOI - 10.1088/1755-1315/769/4/042016
Subject(s) - computer science , hol , rotation formalisms in three dimensions , architecture description language , programming language , software engineering , formal methods , specification language , formal specification , context (archaeology) , software architecture , formal language , software , reference architecture , paleontology , geometry , mathematics , biology
The analysis of safety-critical systems designed by architectural languages such as AADL (Architecture Analysis and Design Language) is a challenging research topic. In such a context, formal methods become an advocated practice in software engineering for rigorous analysis. Moreover, they are applied on specific formalisms to be analyzed on dedicated tools. This paper studies the comprehensive formal specification for AADL language, in particular supporting major components of AADL and Behavior Annex. The presentation of this specification and modeling is the aim of this paper. This work is illustrated with a ARINC653 case study. As a study case, this work develops an AADL model from an ARINC653, specify a set of critical properties of the model and perform formal modeling in in Isabelle/HOL.