[en] Symbolic execution is a well-studied technique for analysing
the behaviour of software components with applications to test case generation. We propose a framework for symbolically executing satellite control procedures and generating test cases based on graph transformation
techniques. A graph-based operational symbolic execution semantics is
defined and the executed procedure models are used for generating test
cases by performing model transformations. The approach is discussed
based on a prototype implementation using the Eclipse Modelling Framework (EMF), Henshin and ECLiPSe-CLP tool ecosystem.