Formalizing operating systems for nano satellites on board computers

In this work we provide a formal verification of the FreeRTOS operating system. Even most, a controller for the system is found. FreeRTOS is one of the most used operating systems for On Board Computers (OBC) in nano satellites such as CubeSats. Exploring, verifying and understating the potential and limitations of OBC operating systems is crucial for the growth of one of the most promising domains in the modern world: the space research industry. FreeRTOS’s formal verification is achieved employing the Feather Weight Visual Scenarios (FVS) framework, which has been previously applied to verify Internet of Things (IoT) protocols.
formal specification, CubeSats, On Board Computers, OBC
Asteasuain, F. (2022). Formalizing operating systems for nano satellites on board computers. En: Congreso Nacional de Ingeniería Informática y Sistemas de Información, CoNaIISI. 10. 3-4 nov 2022, Concepción del Uruguay, Argentina, Buenos Aires : Universidad Tecnológica Nacional.