Robust Resource Partitioning Approach for ARINC 653 RTOS

TL;DR

This paper proposes a static MMU-based architecture for resource partitioning in ARINC 653 RTOS, enhancing guarantees and simplifying verification with minimal runtime overhead across various airborne hardware platforms.

Contribution

It introduces a novel static MMU configuration architecture for ARINC 653 RTOS, improving resource isolation and verification efficiency.

Findings

Implemented on multiple airborne hardware platforms.

Reduced runtime overhead in resource partitioning.

Simplified verification process for memory subsystem.

Abstract

Modern airborne operating systems implement the concept of robust time and resource partitioning imposed by the standards for aerospace and airborne-embedded software systems, such as ARINC 653. While these standards do provide a considerable amount of design choices in regards to resource partitioning on the architectural and API levels, such as isolated memory spaces between the application partitions, predefined resource configuration, and unidirectional ports with limited queue and message sizes for inter-partition communication, they do not specify how an operating system should implement them in software. Furthermore, they often tend to set the minimal level of the required guarantees, for example, in terms of memory permissions, and disregard the hardware state of the art, which presently can provide considerably stronger guarantees at no extra cost. In the paper we present an architecture of robust resource partitioning for ARINC 653 real-time operating systems based on completely static MMU configuration. The architecture was implemented on different types of airborne hardware, including platforms with TLB-based and page table-based MMU. Key benefits of the proposed approach include minimised run-time overhead and simpler verification of the memory subsystem.