This demo shows Smart Play-Out, a new method for executing and analyzing scenario based behavior, which is part of the Play-In/Play-Out methodology and the Play-Engine tool. Behavior is "played in" directly from the system's GUI, and as this is being done the play-engine continuously constructs Live Sequence Charts (LSCs), a powerful extension of sequence diagrams. Later behavior can be "played out" freely from the GUI, and the tool executes the LSCs directly, thus driving the system's behavior.
Smart Play-Out, a recent strengthening of the play-out mechanism, uses verification methods, mainly model-checking, to execute and analyze the LSCs, helping the execution to avoid deadlocks and violations. Thus, Smart Play-Out utilizes verification techniques to run programs, rather than to verify them.
Our approach is especially useful for specifying reactive object-oriented systems, and the LSC language we use has been extended to distinguish between objects and classes and to allow specifying of symbolic scenarios that hold for all object instances of a certain class.
In the demo we will show and explain the tool, illustrating the approach on several applications we have studied, including a phone network, a machine for manufacturing smart-cards and a model of a biological system.
As a long-term goal, for certain kinds of systems the play-out methodology, enhanced by formal verification techniques, could serve as the final implementation too, with the play-out being all that is needed for running the system itself.