We present an example for application of Constraint Handling Rules to automated test data generation and model checking in verification of mission critical software for satellite control.

With the advent of languages such as C++ and Java in mission- and safety-critical space on-board software, new challenges for testing and specifically automated testing arise. In this paper we discuss some of these challenges, consequences and solutions based on an experiment in automated source- code-based testing for C++.