Search SciRate

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.

In the development of modern cockpits, there is a trend towards the use of large displays that combine information about air navigation and the status of aircraft equipment. Flight and equipment performance information generated by multiple flight control systems should be graphically displayed in an easy-to-read form on widescreen multifunction displays. It is usually generated by independent systems whose output must not interfere with each other in accordance with the requirements of the ARINC 653 standard. This paper presents a solution to the problem of displaying ARINC 653 applications, which further improves security and portability, when running multiple applications on a single screen of one physical device.

Existing standards for airborne-embedded software systems impose a number of requirements applicable to the software development cycle of hard real-time operating systems found in modern aircraft. The measures taken are meant to reduce the risks of undesired consequences, but have strongly varying costs. Dynamic instrumentation and static analysis are common practices used to automatically find software defects, from strictly non-conforming code constructions to memory corruptions or invalid control flow. LLVM analyser and sanitizer infrastructure, while regularly applied to general-purpose software, originally was not thought to be introduced to heavily restricted environments. In this paper we discuss the specifics of airborne systems with regards to dynamic instrumentation and provide practical considerations to be taken into account for the effective use of general-purpose instrumentation tools. We bring a complete LLVM stack support to JetOS, a prospective onboard real-time operating system currently being developed at ISP RAS in collaboration with GosNIIAS. As an example, we port AddressSanitizer, MemorySanitizer, and UndefinedBehaviorSanitizer and provide the details against the caveats on all relevant sides: a sanitizer, a compiler, and an operating system. In addition we suggest uninvolved optimisations and enhancements to the runtimes to maximise the effects of the tools.

This paper presents results from the development and evaluation of a deductive verification benchmark consisting of 26 unmodified Linux kernel library functions implementing conventional memory and string operations. The formal contract of the functions was extracted from their source code and was represented in the form of preconditions and postconditions. The correctness of 23 functions was completely proved using AstraVer toolset, although success for 11 functions was achieved using 2 new specification language constructs. Another 2 functions were proved after a minor modification of their source code, while the final one cannot be completely proved using the existing memory model. The benchmark can be used for the testing and evaluation of deductive verification tools and as a starting point for verifying other parts of the Linux kernel.

The paper presents the experience of the authors in model based testing of safety critical real-time control logic software. It describes specifics of the corresponding industrial settings and discusses technical details of usage of UniTESK model based testing technology in these settings. Finally, we discuss possible future directions of safety critical software development processes and a place of model based testing techniques in it.