—In this case study we test a landing gear control system of a military aircraft with the new version of LUTESS, a tool for testing automatically synchronous software. LUTESS requires the tester to specify the environment of the software under test by means of invariant properties in order to guide the test data generation. This specification can be enriched by operational profile specification in order to obtain more realistic scenarios. Moreover, test generation guided by safety properties makes possible to test more thoroughly the key features of the software, possibly under hypotheses on the software behaviour. In this case, the generator chooses input data which are able to violate the properties. The new version of LUTESS is based on constraint logic programming and provides some additional features (numeric inputs and outputs, hypotheses for safety guided testing, more powerful operational profiles). In this paper, we present the necessary steps for building the test model...