SMT-Based Cost Optimization Approach for the Integration of Avionic Functions in IMA and TTEthernet Architectures

The design of avionic systems is a complex engineering activity. The iterative integration approach helps in controlling the complexity of such activity. On the other hand, using such approach to design evolving systems requires the reconfiguration of scheduling parameters of already integrated parts. This reconfiguration results in a recertification process having a cost that depends on the criticality level of the affected application. We propose a new approach which helps the system designer at each integration step in establishing the new scheduling parameters that minimize such cost. In this work, we focus on the Integrated Modular Avionic (IMA) architecture connected through a Time-Triggered Ethernet (TTEthernet) network. We present a formal model for such systems and we use this model to define a set of constraints that ensure the real-time requirements. These constraints are expressed using an SMTbased language and we used the SMT-solver YICES to find automatically a feasible scheduling parameters that minimize the cost of integration. We show our framework at work by analyzing the iterative integration of some functionalities of the Flight Management System.