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

飞机的增量认证要求航空电子系统采用基于模型的设计，越来越依赖于综合模块化航空电子技术(IMA)。IMA定义了一种允许减小尺寸、重量和功率(交换)的分布式体系结构，并得到了几个标准的支持，例如ARINC 653(用于集成共享分布式硬件资源的混合关键程度的航空电子功能的接口)。为了提高可靠性和简化集成过程，时间触发体系结构(TTA)为新的同步通信设备提供了理论框架。TTA为分布式系统提供了可靠的同步机制，最近被实现为TTETHERNET协议，允许高性能和强大的实时保证，同时仍封装异步通信。IMA和TTA都将混合关键组件隔离到分区中，以实现更安全的集成。事实上，IMA使应用程序能够通过在分布式实时操作系统(RTOS)上在空间上(内存区)和时间上(处理器调度)进行分区来安全地交互，而TTA允许分布式软件和硬件通过时分多址(TDMA)在这些RTOS之间安全地通信，即通过将带宽划分为时隙(网络调度)。IMA和TTA的结合使用使得航空电子系统的基于模型的设计本质上侧重于通过静态定义资源分配和混合临界分区交互来进行集成。虽然IMA和TTA已经在文献中得到了研究，但它们与ARINC 653和TTETHERNET实现的集成还没有被解决。为了能够对下一代航空电子系统进行基于模型的验证和验证，我们将定义一个受到AADL和UMLMarte等标准建模语言(组合)启发的正式框架。该项目的目标是提供一个基于模型的集成平台，使用实时调度、仿真和形式验证方法，所有这些方法都是为结合IMA和TTA的系统定制的。

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.