Several studies have shown that automated testing is a promising approach to save significant amounts of time and money in the industry of reactive software.But automated testing requires a formal framework and adequate means to generate test data.In the context of synchronous reactive software, we have built such a framework and its associated tool -Lutess-to integrate various well-founded testing techniques.This tool automatically constructs test harnesses for fully automated test data generation and verdict return.The generation conforms to different formal descriptions: software environment constraints, functional and safety-oriented properties to be satisfied by the software, software operational profiles and software behavior patterns.These descriptions are expressed in an extended executable temporal logic.They correspond to more and more complex test objectives raised by the first pre-industrial applications of Lutess.This paper concentrates on the latest development of the tool and its use in the validation of standard feature specifications in telephone systems.The four testing techniques which are coordinated in Lutess uniform framework are shown to be well-suited to efficient software testing.The lessons learnt from the use of Lutess in the context of industrial partnerships are discussed.

Test data generation and test execution are both time-consuming activities when done manually. Automated testing methods promise to save a great deal of human effort. This especially applies to reactive programs which have complex behaviour over time and which require long test sequences. We present Lutess, a testing environment for synchronous reactive software. Lutess produces automatically and dynamically test data with respect to some environment constraints of the program under test. Moreover, it allows to trace the test execution and spot the situations where the program violates its properties. Lutess offers several specification-based testing methods. They aim at simulating more realistic environment behaviours, producing relevant data to test thoroughly a given property or driving the program under test into interesting situations. To produce the test data, the methods use different types of guides: statistical distribution of the input generation, properties, or behavioural patterns. Lutess proved to be powerful and easy to use in industrial case studies. Lutess won the Best Tool Award of the first Feature Interaction Detection Contest. The tool is described from a practical point of view.