Using Reactive Synthesis:
An End-to-End Exploratory Case Study
Abstract
Reactive synthesis is an automated procedure to obtain a
correct-by-construction reactive system from its temporal
logic specification. Despite its attractiveness and major
research progress in the past decades, reactive synthesis
is still in early-stage and has not gained popularity outside
academia.
We conducted an exploratory case study in which
we followed students in a semester-long university workshop
class on their end-to-end use of a reactive synthesizer,
from writing the specifications to executing the synthesized
controllers. The data we collected includes more than 500
versions of more than 80 specifications, as well as more
than 2500 Slack messages, all written by the class participants.
Our grounded theory analysis reveals that the use of reactive
synthesis has clear benefits for certain tasks and that adequate
specification language constructs assist in the specification
writing process. However, inherent issues such as unrealizabilty,
non-well-separation, the gap of knowledge between the users and
the synthesizer, and considerable running times prevent reactive
synthesis from fulfilling its promise. Based on our analysis,
we propose action items in the directions of language and
specification quality, tools for analysis and execution,
and process and methodology, all towards making reactive
synthesis more applicable for software engineers.
Dor Ma'ayan and Shahar Maoz, Using Reactive Synthesis: An End-to-End Exploratory Case Study. Proc. of ICSE 2023. To appear.