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 ...

• Type: Conference
• Year: 2007
• Where: OOPSLA
• Authors: Hillel Kugler, Cory Plock, Amir Pnueli
• Keywords: Executable Trace, LSC Requirements, OOPSLA 2007, Smart Play-out