This blog was written by Dr.-Ing. Martin Halle and highlights the ELISA Project Aerospace Working Group’s first steps toward using Linux safely in flight.
The ELISA Project Aerospace Working Group is actively developing use cases designed to improve Linux architecture and related tools. The overarching goal is to pave the way for using Linux safely in avionics at various levels of criticality.
To lay the flight path for these ambitious goals, the working group has released a new demonstration focusing on a lower-criticality use case, serving as an essential first step toward using Linux in flight.
The Cabin Light Use Case
The new demonstration showcases a system that would operate an aircraft’s cabin lights. Specifically, we show how to measure the system’s compliance with strict timing expectations. While the Light Server and Light App are based on Python, the core of the verification process relies on robust, aerospace-grade monitoring. Any system output is written to a log file in a syslog style, which is then shown live using the Linux “tail” command.
Ensuring Reliability with Copilot
To monitor our timing expectations, the demonstration makes use of the Copilot runtime verification framework, a tool designed specifically for hard real-time systems.
What is Copilot?
- It is an open-source temporal programming language.
- It compiles to C99 with predictable time and memory bounds.
- It is routinely used by NASA to write and verify critical systems both in aerospace and on the ground.
In this specific demo, we use Copilot to express the temporal properties we expect of a real-time Linux kernel operating in the aerospace domain. For example, the framework ensures that a cabin light will actually turn on or off within a limited amount of time when a demand is made. Copilot acts as a watchdog, monitoring this specific property and reporting whenever there are any violations.
Get Involved and Learn More
This video and demonstration are part of the broader ELISA Aerospace Working Group initiative. We invite developers, engineers, and aerospace enthusiasts to explore the code, replicate the demo, and contribute to the future of open-source avionics.
Explore the Resources:
- Check out the Aerospace WG repository.
- Subscribe to the Aerospace mailing list.
- Follow the step-by-step instructions to run the demonstration yourself.
- Explore the Copilot Language on Github.
- Keep up to date by subscribing to the ELISA Project newsletter or connect with us on LinkedIn
- Join the conversation with the ELISA community on Discord