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

嵌入时间触发架构中的混合关键性航空电子系统的基于模型的集成和验证

• 批准号: 435325-2012
• 负责人: Mullins, John
• 金额: $ 6.4万
• 依托单位: École Polytechnique de Montréal
• 依托单位国家: 加拿大
• 项目类别: Collaborative Research and Development Grants
• 财政年份: 2013
• 资助国家: 加拿大
• 起止时间: 2013-01-01 至 2014-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=533172
• 关键词: Model; based; integration; verificafion; mixed

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.

飞机的增量认证构成了基于模型的航空系统设计，越来越多地依靠集成的模块化航空电子（IMA）。 IMA定义了一个分布式体系结构，允许减小尺寸，重量和功率（交换），并得到多种标准（例如ARINC 653）（用于集成混合关键性共享分布式硬件资源的航空功能的接口）。为了提高可靠性并简化集成过程，时间触发的体系结构（TTA）为新的同步通信设备提供了理论框架。 TTA为分布式系统提供了可靠的同步机制，最近已作为TTETERNET协议实施，可以具有强大的实时保证的高性能，同时仍封装异步通信。 IMA和TTA都将混合批判性组件分隔为分区，以进行更安全的集成。实际上，IMA可以通过空间（内存区）和时间（处理器时间表）对分布式实时操作系统（RTOS）进行空间（记忆区）（处理器计划）的分区来安全互动，而TTA允许分布式软件和硬件可以通过时间分组多访问（TDMA）安全地在这些RTO之间进行安全通信，即通过将bandwidth分配到时间分段（即网络时间段）（网络时间表（网络））。 IMA和TTA的联合使用使基于模型的航空系统设计基本上是通过对资源分配和混合批判性分区相互作用的静态定义进行集成。尽管IMA和TTA已经在文献中进行了研究，但它们与ARINC 653和TTERNET的实施的整合尚未得到解决。为了允许基于模型的验证和对下一代航空系统的验证，我们将定义一个正式的框架，该框架灵感来自（组合）标准建模语言，例如AADL和UML MARTE。该项目的目的是使用实时调度，模拟和正式验证方法提供基于模型的集成平台，所有这些都针对结合IMA和TTA的系统量身定制。