To help support future missions we are currently working on a CubeSat "operating system" that we are calling CubedOS. Despite the name, CubedOS is really more of an application framework than a true operating system. It builds on the services provided by the underlying Ada runtime system, namely tasking support, which in turn are built (may be built) on top of some underlying host operating system.
Yet the intent of CubedOS is to serve an operating system-like role in the construction of CubeSat flight control software. It provides several common services needed by most, if not all, missions such as non-critical timing and background processing, a file system, a high level runtime library, and a driver model. CubedOS thus simplifies the construction of flight software by relieving the application developer of the burden of repeatedly providing these basic services.
At its core CubedOS provides a general purpose, asynchronous message passing facility that is used by CubedOS modules for inter-module communication. Because of the asynchronous messages, CubedOS applications can easily exhibit a high degree of concurrency. In addition, application developers do not need to separately design every communication path between interacting tasks; pre-built CubedOS messages should often be sufficient.
However, the message passing design of CubedOS also presents some challenges. The overhead of message passing may be unacceptable in some situations. We anticipate that some time critical interactions between tasks will still need to be hand designed. Furthermore the effect of the message passing architecture on the static analysis of CubedOS programs has yet to be fully explored. There is a potential loss of static type safety in the current architecture. Furthermore the ability for any module to asynchronously send a message to any other module (using potentially non-empty mailboxes) will likely complicate any real-time analysis required by the application. We intend to explore these issues further as we go forward. In the meantime our preliminary experiments with CubedOS do indicate that the architecture can simplify the construction of highly concurrent systems.
One might reasonably ask: why not just use the services of some suitable embedded operating system and be done with it? The main reason is our requirement to use SPARK and to insist on verifying freedom from runtime errors (at least). Most existing embedded operating systems are written in C and thus prone to errors that verified SPARK programs are not. That said, there do exist certified embedded operating systems that could potentially take over some of the functionality offered by CubedOS. Their use would allow us to replace certain packages in CubedOS with wrappers that simply enclose services provided by an underlying system while maintaining compatibility with CubedOS applications. We intend to explore this option in the future as well.