Paper Info
Title
Validating, verifying and testing timed data-flow reactive systems in Coq from controlled natural-language requirements.
Abstract
Data-flow reactive systems (DFRSs) form 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 these 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; general and domain-specific system property verification is supported by the development of proof scripts, and test generation is achieved with the aid of the QuickChick tool. 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%. (C) 2020 Elsevier B.V. All rights reserved.
Year
DOI
Venue
2021
10.1016/j.scico.2020.102537
SCIENCE OF COMPUTER PROGRAMMING
Keywords
DocType
Volume
Timed data-flow reactive system,Interactive theorem proving,Property-based testing,Controlled natural language
Journal
201
ISSN
Citations 
PageRank 
0167-6423
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Gustavo Carvalho1486.13
Igor Meira200.34