CubedOS: A Verified CubeSat Operating System

摘要

In this paper we present CubedOS, a lightweight application framework for CubeSat flight software. CubedOS is written in SPARKand proved free of certain classes of runtime errors. It consists of a collection of interacting, concurrent modules that communicate via message passing over a microkernel based on Ada's Ravenscar tasking model. It provides core services such as, for example, communication protocol processing and publish/subscribe message handling. Application-specific modules can be added to provide both high level functions such as navigation and power management, as well as low level device drivers for mission-specific hardware.%SPARK; student project; CubeSat