End-to-End Verification of Initial and Transition Properties of GR(1) Designs Generated by Salty in SPARK.pdf
Presented as part of the 2020 HCSS conference.
| Manual design of control logic for reactive systems is a time-consuming and error-prone process. An alternative is to automatically generate controllers from high-level specifications using “correct-by-construction” synthesis approaches. Recently, there has been interest in synthesizing controllers from Generalized Reactivity(1) or GR(1) specifications, since computational complexity is relatively low. Several tools for synthesis from GR(1) specifications now exist and have been used to generate controllers for aircraft power distribution, software-defined networks, ground robots, and teams of unmanned aerial vehicles, to name a few. Here, we discuss Salty, an open-source tool that aids synthesis from GR(1) specifications. Salty addresses three shortcomings of existing synthesis tools.
|
First, it makes specifications easier to write and debug by supporting features such as richer input and output types, user-defined macros, common specification patterns, and specification optimization and sanity checking. Second, it produces software implementations of synthesized controllers in a variety of languages, rather than simply producing controller design descriptions. Third, though synthesis from GR(1) specifications is theoretically “correct-by-construction,” errors in tool implementation can lead to errors in synthesized controllers, so we have extended Salty to produce controllers in SPARK. SPARK is both a language and associated set of verification tools that has the potential to enable “end-to-end'' verification of synthesized controllers with respect to their original GR(1) specifications. To date, SPARK is able to automatically verify that synthesized controllers of modest (though not trivial) size satisfy a subset of properties comprising their original GR(1) specifications, namely system initial and transition properties.
In this talk, we introduce GR(1), some of its applications, Salty, and SPARK. We then describe how we encode synthesized controllers in SPARK, along with the necessary contracts and assertions needed for SPARK to verify system initial and transition properties properties automatically, i.e. without requiring additional annotations from the user. Since GR(1) specifications encode assumptions about the environment in which the controlled system operates, we discuss how we handle these assumptions in the implementation, since there are several reasonable choices. We also discuss ideas for increasing the size of synthesized controllers that can be verified by SPARK. And finally, we discuss possible approaches for verifying the full set of GR(1) properties, i.e. including liveness.