Sciweavers

OOPSLA
2007
Springer

Synthesizing reactive systems from LSC requirements using the play-engine

14 years 5 months ago
Synthesizing reactive systems from LSC requirements using the play-engine
Live Sequence Charts (LSCs) is a scenario-based language for modeling object-based reactive systems with liveness properties. A tool called the Play-Engine allows users to create LSC requirements using a point-and-click interface and generate executable traces using features called playout and smart play-out. Finite executable trace fragments called super-steps are generated by smart play-out in response to user inputs. Each super-step is guaranteed not to violate the LSC requirements, provided one exists. However, non-violation is not guaranteed beyond each individual super-step. In this work, we demonstrate a powerful extension to smart play-out which produces only traces that are guaranteed not to violate the LSC requirements, provided the requirements are realizable. Using this method, we may synthesize correct executable programs directly from LSC requirements. Categories and Subject Descriptors D.2.1 [Software Engineering]: Requirements/specifications—languages, tools; D.2.2 ...
Hillel Kugler, Cory Plock, Amir Pnueli
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where OOPSLA
Authors Hillel Kugler, Cory Plock, Amir Pnueli
Comments (0)