Abstract:

   
A novel approach to behavioral requirements for reactive systems
is described, in which scenario-based requirements are "played in"
directly from the system's GUI or some abstract version thereof,
and behavior can then be "played out" freely, adhering to all the
requirements. The approach is supported and illustrated by a
tool we have built --  the play-engine.  We will also describe a
"smart" play-out mode, whereby parts of the plan for execution
are computed using model-checking. Thus, we employ formal
verification techniques for driving the execution. The approach
appears to be useful in many stages in the development
of reactive  systems, and could also pave the way to systems that
are constructed directly from their requirements, without the need
for intra-object or intra-component modeling or coding at all.