Towards a Testing Methodology for Reactive Systems: A Case Study of a Landing Gear Controller

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 behavior. 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 for Lutess on a real case study from the avionics. This makes possible to better understand the applicability of the approach and to assess the difficulty and the effectiveness of such a process in real-world applications.