CubedOS is an operating system intended for CubeSat flight control software. The intent is for CubedOS to be general enough and modular enough for other groups to profitably employ the system. Since every mission uses different hardware and has different software needs, CubedOS is a really an application framework into which custom modules can be plugged to implement whatever mission functionality is required. CubedOS provides inter-module communication and other common services required by many missions. CubedOS thus serves both as a kind of operating system and as a library of useful tools.
CubedOS is written in SPARK with the goal of verifying the code to be free of runtime error. It is our intention to also use SPARK to prove some other correctness guarantees to whatever extent is practical. Normally all CubedOS modules will also be written in SPARK and proved free of runtime error (at least). However, CubedOS also allows modules, or parts of modules, to be written in full Ada or even C if appropriate. This allows CubedOS to take advantage of third party C libraries or to integrate with an existing C code base.
CubedOS can run directly on top of the hardware, with the assistance of a suitable Ada runtime system. It can also run as an ordinary process on top of a conventional operating system such as Linux, or on top of an embedded operating system such as VxWorks. This is made possible by the CubedOS low-level abstraction layer (LLAL). This layer plays a role in CubedOS similar to that played by the hardware abstraction layer used by many conventional operating systems. To port a CubedOS application to a new platform or underlying operating system, one should only need to provide a suitable LLAL.
The architecture of CubedOS is a collection of active and passive modules, where each active module contains one, and sometimes multiple, threads or tasks. Although CubedOS is written in SPARK/Ada there need not be a one-to-one correspondence between CubedOS modules and Ada packages. In fact, modules are routinely written as a collection of Ada packages in a package hierarchy, allowing complex modules to be implemented with the help of internal private child packages.
Critical to the plug-and-play nature of CubedOS, each active module is self-contained and does not make direct use of any code in any other active module (although passive modules serving as library components can be used). All inter-module communication is done through the CubedOS infrastructure with no direct sharing of data or executable content. In this respect CubedOS modules are similar to processes in a more conventional operating system. One consequence of this policy is that a library that several modules want to use must be either duplicated in each module or provided as an independent (passive) module of its own.
In the language of operating systems, CubedOS can be said to have a microkernel architecture where task management is provided by the Ada runtime system. Both low level facilities, such as device drivers, and high level facilities, such as communication protocol handlers or navigation algorithms, are all implemented as CubedOS modules. All modules are treated equally by CubedOS.
In addition to inter-module communication, CubedOS provides several general purpose facilities. In some cases only the interface to the facility is described and different implementations are possible (even encouraged). Having a standard interface allows other components of CubedOS to be programmed against that interface without concern about the underlying implementation.
- An asynchronous message passing system with mailboxes. This, together with the underlying Ada runtime system constitutes the "kernel" of CubedOS.
- A runtime library of useful packages, all verified with SPARK.
- A real time clock module.
- A file system interface.
- A radio communications interface.
- Modules providing support for CCSDS protocols.
A CubedOS system also requires drivers for the various hardware components in the system. Although the specific drivers required will vary from mission to mission, CubedOS does provide a general driver model that allows components to communicate with drivers fairly generically. In a typical system there will be low level drivers for accessing hardware busses as well as higher level drivers for sending/receiving commands from components such as the radio, the power system, the camera, etc. The low level drivers constitute the CubedOS LLAL.
CubedOS provides several advantages over "home grown" frameworks.
- The message passing architecture is highly concurrent and allows many overlapping activities to be programmed in a natural way. For example, our implementation of the CCSDS File Delivery Protocol (CFDP) takes advantage of this.
- The architecture provides a lot of runtime flexibility; programs can adapt their communication patterns at runtime.
- The architecture is consistent with the restrictions of Ada's Ravenscar profile.
CubedOS also brings several disadvantages over more customized solutions.
- Because CubedOS messages are just octet sequences, there is runtime overhead associated with encoding and decoding them.
- CubedOS sacrifices some static type safety; decoded messages must be validated at runtime with type errors being handled during the validation process. This is particularly worrisome in light of CubedOS's goal of providing robust assurances of correctness.
- Currently (June 2016) the SPARK tools have difficulty analyzing the CubedOS mailbox array. This is due to limitations on the tools' ability to track information flow through individual array elements. To resolve this problem will require some redesign of the CubedOS infrastructure and/or sacrificing the use of SPARK in certain parts of the system.
CubedOS is an ongoing effort and should be considered experimental at this time. However, we hope to refine the architecture and implement enough non-trivial services to make CubedOS useful to other groups. Our long term goal is to distribute CubedOS to others working on CubeSat software or, for that matter, other similar embedded systems.
Relationship to cFE/cFS
NASA Goddard has an open source project called cFE/cFS (for "Core Flight Executive" and "Core Flight System"). This system shares many of the same goals as CubedOS. In particular it provides an infrastructure (cFE) with a modular architecture and several core modules of interest to many missions (cFS). Unlike CubedOS, cFE/cFS is a mature system with a significant user community and well evolved software components. However, cFE/cFS is not written in a verifiable language. One of the main goals of the CubedOS project is to develop a framework that is verifiable. This is the critical difference between CubedOS and cFE/cFS.