A powerful methodology for specifying scenario-based requirements of reactive systems is described, in which the behavior is "played in" directly from the system's GUI or some abstract version thereof, and can then be "played out". The approach is supported and illustrated by a tool, which we call the play-engine. As the requirements are played in, the play-engine automatically generates a formal version in the language of live sequence charts (LSCs). As they are played out, it causes the application to react according to the universal ("must") parts of the specification; the existential ("may") parts can be monitored to check their successful completion.
Play-in is a user-friendly high-level way of specifying behavior and play-out is a rather surprising way of working with a fully operational system directly from its inter-object requirements. The play-out execution mechanism is enhanced with a "smart" play-out module, in which verification techniques, mainly model-checking, are used both to drive the model and to satisfy system tests, expressed as existential LSCs.
The ideas appear to be relevant to many stages of system development, including requirements engineering, specification, testing, analysis and implementation.
The Israeli Workshop on Programming Languages & Development Environments