H. Kugler, C. Plock, and A. Pnueli
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 play-out 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.
In Companion to the 22nd ACM SIGPLAN conference on object oriented programming systems and applications (OOPSLA’07)