Rigorous software design for nano and micro satellites using BIP framework

The CubETH satellite mission, a cooperative Swiss CubeSat mission involving ETH Zurich, EPF Lausanne, several universities of applied sciences, and Swiss companies, will allow technology demonstrations and proof-of-concepts concerning GNSS-based navigation information by carrying five patch antennas, each connected to two independent u-blox NEO-7N receivers. These very small, commercially available low-cost receivers are able to track single-frequency code and phase data of all the major GNSS, i.e. GPS, GLONASS, QZSS, Galileo and Beidou. The main science objective for the CubETH mission is to investigate precise orbit determination strategies using COTS hardware. The mission shall also demonstrate new technologies, applicable in the field of small satellites. In this work, we focus mostly on development of robust flight software for small and nano satellites. During the Swisscube project there were numerous problems with validation and verification of the flight software code. The software has to be adapted to the hardware architecture selected for every new satellite mission. While commercial tools exist to help with the issue, subject of robust software development was not addressed by the cubesat community, mostly due to lack of resources. Some projects simply structure their code in C/C++ and then extensively test it, maybe using some analysis tools such as "Lint" [5]. This is an helpful tool to find some design errors, but it does not guarantee that the software behavior is the desired one. Others use SysML/UML tools to describe the system as a whole and then check some properties such as energy consumption. SysML can be a valid tool for system engineering as a whole, but it is not rigorous enough to allow automatic software behavior verification and validation. In this project the “Behavior Interaction Priority” BIP framework will be used to design the software running in the control and data management subsystem (CDMS) of CubETH. The BIP framework has been developed by the Verimag laboratory in Grenoble university and is currently used in the EPFL by the "Rigorous System Design Laboratory" (RISD). We have designed and modeled a full software architecture using this framework to formally verify our software. We will present lessons learned and problems that were encountered during the development.