Specifying Avionic Embedded Systems by Denotations of the Time-Triggered Constraint-Based Calculus

The Integrated Modular Avionics (IMA) architecture and the Time-Triggered Ethernet (TTEthernet) network have emerged as the key components of a typical architecture model for recent civil aircrafts. It has recently been proposed to model both the (IMA) architecture and the TTEthernet network in the constraint-based TTCC calculus. In this paper, we show how the declarative aspects of this calculus can provide a simple and elegant way to specify requirements of time-triggered systems. We illustrate our approach on a complete model of a sub-system of the flight management system.