Formal Modelling of Avionics Systems. An Approach Based on Category Theory and the EXPRESS Modelling Language

In previous work, we defined a component oriented framework dedicated to the specification of embedded systems in the aeronautics domain. A component is defined as a formal entity with three internal layers together with a collection of models defined in domain-oriented views. A categorical framework has been proposed to provide a unified representation of the component calculus as well as the various formal models used for the analysis of the system. In this paper, we present an implementation of this categorical framework using the EXPRESS data modelling language. EXPRESS is used to give an operational representation of the formalization, which is quite different from classical implementations of category theory based approaches.