Speakers:  Shahar Maoz (TAU) and Smadar Szekely (WIS)

Title: Counter Play-Out: Executing Unrealizable Scenario-Based Specifications

Abstract: The scenario-based approach to the specification and
simulation of reactive systems has attracted much research efforts in
recent years. While the problem of synthesizing a controller or a
transition system from a scenario-based specification has been studied
extensively, no work has yet effectively addressed the case where the
specification is unrealizable and a controller cannot be synthesized.
This has limited the effectiveness of using scenario-based
specifications in requirements analysis and simulation.
In this work we present counter play-out, an interactive debugging
method for unrealizable scenario-based specifications. When we
identify an unrealizable specification, we generate a controller that
plays the role of the environment and lets the engineer play the role
of the system. During execution, the former chooses environment’s
moves such that the latter is forced to eventually fail in satisfying
the system’s requirements. This results in an interactive, guided
execution, leading to the root causes of unrealizability. The
generated controller constitutes a proof that the specification is
conflicting and cannot be realized.
Counter play-out is based on a counter strategy, which we compute by
solving a Rabin game using a symbolic, BDD-based algorithm. The work
is implemented and integrated with PlayGo, an IDE for scenario-based
programming developed at the Weizmann Institute of Science. Case
studies show the contribution of our work to the state-of-the-art in
the scenario-based approach to specification and simulation.

The presentation in the seminar will include live demonstration of
PlayGo, and the results of  the paper describing counter play-out
by Shahar Maoz and Yaniv Sa’ar that will appear at ICSE’13.