Modelling and testing timed data-flow reactive systems in Coq from controlled natural-language requirements

TL;DR

This paper presents a framework using Coq to specify, verify, and test data-flow reactive systems automatically derived from natural language requirements, improving formal guarantees and testing efficiency.

Contribution

It introduces an automated method to derive Coq specifications from natural language requirements and integrates property verification with testing in a unified framework.

Findings

Achieved an average mutation score of 75.80% within 8 seconds.

Demonstrated the approach on aerospace industry examples.

Enhanced testing performance and defect detection in DFRS models.

Abstract

Data-flow reactive systems (DFRSs) 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 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 and verify DFRS models. Moreover, the specification of DFRSs in Coq is automatically derived from controlled natural-language requirements. Property verification is defined in both logical and functional terms. The latter allows for easier proof construction. Tests are generated with the support of the QuickChick tool. Considering examples from the literature, but also from the aerospace industry (Embraer), our testing strategy was evaluated in terms of performance and the ability to detect defects generated by mutation; within 8 seconds, we achieved an average mutation score of 75.80%.