Verification of the C++-Operating System RODOS in Context of a Small-Satellite

Within the small satellite mission TechnoSat of Technische Universitaet Berlin, a verification strategy based on Dynamic Analysis has been applied to the C++-operating system RODOS using automated massive stimulation of the softwareunder- test. This approach is aiming at evaluating the robustness of the software and to derive feedback on the implemented messaging scheme of the on-board process chain. For fault detection and recording of message exchange the code is automatically instrumented with application-independent indicators which shall flag anomalies. Manual fault analysis is limited to the reported issues highlighting fault potential in contrast to usual reviews on the full code. The suggested reviews were extended to similar code, an approach which turned out as being effective. For the verification of the messaging scheme observed functional and performance properties were evaluated. The verification strategy targets the reduction of costs of verification and risks. Within this paper, the different verification steps are described and examples for reported issues are given.