Reactive synthesis specification review for validity and quality - Software and Systems Modeling

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. While the synthesized system is guaranteed to be correct w.r.t. the specification, the specification itself may not reflect the intended requirements and hence requires validation. Beyond validity, the specification may have quality issues that may impair its readability and maintainability. In this work, we adapt ideas from software engineering and formal verification to present new methods for the validation and the detection of quality issues in reactive system specifications for synthesis. Our first contribution provides a method for specification validation based on a systematic exploration of the specification elements. Specifically, we present algorithms to generate a small scenario suite that demonstrates the meaning of each element in the specification in the context of the behaviors of a controller that is synthesized from it. Our second and third contributions provide means for the detection of quality issues in the specification. Specifically, we present algorithms to detect unnecessary variables that appear in specification elements as well as to detect fine-grained syntactic and semantic specification clones and suggest corresponding refactoring. An important characteristic of our work is that both the algorithms and the controller representation are symbolic. This allows our work to scale well to specifications over large state spaces. We have implemented our ideas in the Spectra synthesis environment and evaluated performance and effectiveness over benchmarks from the literature.