Validating, verifying and testing timed data-flow reactive systems in Coq from controlled natural-language requirements

Abstract

The NAT2TEST strategy provides means for generating test cases from controlled natural-language requirements. It is tailored for testing timed data-flow reactive systems (DFRSs), which are a class of embedded systems whose inputs and outputs are always available as signals. Input signals can be seen as data provided by sensors, whereas the output data are provided to system actuators. In previous works, verifying well-formedness properties of DFRS models was accomplished in a programmatic way, with no formal guarantees, and test cases were generated by translating theses models into other notations. Here, we use Coq as a single framework to specify, validate and verify DFRS models. Moreover, the specification of DFRSs in Coq is automatically derived from controlled natural-language requirements, and well-formedness properties are formally verified with no user intervention. System validation is supported by bounded exploration of models, and test generation is achieved with the aid of the QuickChick tool. Our Coq-based testing strategy was integrated into the NAT2TEST tool, which is a multi-platform tool written in Java, using the Eclipse RCP framework. Considering examples from the literature, but also from the aerospace (Embraer) and the automotive (Mercedes) industries, our automatic testing strategy was evaluated in terms of performance and the ability to detect defects generated by mutation. Within seconds, test cases were generated automatically from the requirements, achieving an average mutation score of about 75%. Discarding equivalent mutants, in one of the industrial examples, the actual mutation score is 100%; the generated test cases were capable of detecting all systematically introduced errors.