Model-based integration and verificafion for mixed-criticality avionics systems embedded in a time-triggered architecture

点击翻译按钮获取中文摘要

Incremental certification of airplanes imposes a model-based design of avionic systems, relying more and more on Integrated Modular Avionics (IMA). IMA defines a distributed architecture allowing the reduction of size, weight, and power (SWaP) and is supported by several standards, such as ARINC 653 (an interface for the integration of avionic functions of mixed criticality sharing distributed hardware resources). In order to increase dependability and ease the integration process, the Time-Triggered Architecture (TTA) offers a theoretical framework for new synchronous communication devices. TTA offers a reliable synchronization mechanism for distributed systems and has recently been implemented as the TTEthernet protocol, allowing high performance with strong real-time guarantees while still encapsulating asynchronous communications. Both IMA and TTA segregate mixed-criticality components into partitions for a safer integration. Indeed, IMA enables applications to interact safely by partitioning them spatially (memory zones) and temporally (processor schedules) over distributed Real-Time Operating Systems (RTOS), while TTA allows distributed software and hardware to communicate safely between these RTOS through Time Division Multiple Access (TDMA), i.e., by partitioning bandwidth into time slots (network schedules). The combined use of IMA and TTA makes model-based design of avionic systems focus essentially on the integration through the static definition of resource allocation and mixed-criticality partitions interaction. Although IMA and TTA have already been studied in the literature, their integration with their implementations as ARINC 653 and TTEthernet has not yet been addressed. In order to allow model-based verification and validation of next-generation avionic systems, we will define a formal framework inspired from (a combination of) standard modeling languages such as AADL and UML MARTE. The goal of this project is to offer a model-based integration platform using real-time scheduling, simulation and formal verification approaches, all tailored for systems combining IMA and TTA.