End-to-End Verification of Initial and Transition Properties of GR(1) Designs in SPARK

Manually designing control logic for reactive systems is time-consuming and error-prone. An alternative is to automatically generate controllers using “correct-by-construction” synthesis approaches. Recently, there has been interest in synthesis from Generalized Reactivity(1) or GR(1) specifications, since the required computational complexity is relatively low, and several tools exist for synthesis from GR(1) specifications. However, while these tools implement synthesis approaches that are theoretically “correct-by-construction,” errors in tool implementation can still lead to errors in synthesized controllers. We are therefore interested in “end-to-end” verification of synthesized controllers with respect to their original GR(1) specifications. Toward this end, we have modified Salty – a tool that produces executable software implementations of controllers from GR(1) specifications in a variety of programming languages – to produce implementations in SPARK. SPARK is both a programming language and associated set of verification tools, so it has the potential to enable the “end-to-end” verification we desire. In this paper, we discuss our experience to date using SPARK to implement controllers and verify them against a subset of properties comprising GR(1) specifications, namely system initial and system transition properties. We also discuss lessons learned about how to best encode controllers synthesized from GR(1) specifications in SPARK for verification, examples in which verification found unexpected controller behaviors, and caveats related to the interpretation of GR(1) specifications.