Dr. Jan Oliver Ringert, Tel Aviv University, Israel:On Challenges in Reactive Synthesis for Software Engineers: Support for LTL Specification Patterns and a Case Study

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. Despite recent advancements on the theory and algorithms of reactive synthesis, many challenges remain in bringing reactive synthesis technologies to the hands of software engineers. GR(1) is a well-known fragment of linear temporal logic introduced by Piterman et al. where synthesis is possible using a polynomial symbolic algorithm. One challenge in making the GR(1) fragment useful for software engineers is its restricted syntax.
Further challenges relate to the change from writing code to writing specifications, and the development of tools to support a specification-centric rather than a code-centric development process. We report on our work in progress to investigate whether the well-known high-level specification patterns identified by Dwyer et al., which are common in industrial specifications and make writing specifications easier, can be supported in GR(1) synthesis. Specifically, we show that 52 out of the 55 patterns of Dwyer et al. can be supported, and present an automated, sound and complete translation of supported patterns to the GR(1) form, which effectively results in a catalogue and an efficient reactive synthesis procedure for any specification that is written using the patterns. Next, we report  on a case study we have conducted to learn about the challenges of using GR(1) synthesis in the development of a reactive robotic system.
In the case study we developed a specification of a forklift controller, deployed on a Lego robot. The case study employs LTL specification patterns as an extension of the GR(1) specification language and an examination of two specification variants for execution scheduling. We present the specifications we developed, our observations, and challenges faced during the case study. Joint work with Shahar Maoz.

Supported by ERC StG SYNTECH.
S. Maoz and J. O. Ringert. GR(1) Synthesis for LTL Specification Patterns. Proc. of ESEC/FSE 2015, ACM.

S. Maoz and J. O. Ringert. Synthesizing a Lego Forklift Controller in GR(1): A Case Study. SYNT 2015: 4th Workshop on Synthesis (with CAV).

Bookmark the permalink.