IST-2001-33522 OMEGA

Correct Development of Real-Time Embedded Systems

The OMEGA toolset

The OMEGA toolset
     Timed system verification
     Untimed system verification
     PVS tools
     LSC tools
The OMEGA UML profile
Case studies
Publications and bibliography
Download documents
Partners & Persons
Related links

Tool description
Weizmann Institute of Science 

Tool description

The Play-Engine tool supports a scenario-based approach for specifying and executing behavioral requirement of complex reactive systems. Scenarios are specified using the language of live sequence charts (LSCs) [1], a powerfull extension of the classical message sequence charts.  A main new paradigm supported is a method called the  play-in/play-out approach [2].  It supports a convenient way to capture requirements by playing them in using a graphical user interface (GUI), and a rather surprizing and powerful method for executing the requirements directly.  An extension of this approach called smart play-out [3] uses verification methods to execute the scenarios directly, and also supports methods for analyzing the scenarios for consistency and and satisfaction of given behavioral properties.

The following sections provide some more detail on these topics and additional related extensions.

  • Play-In : The main idea of the play-in process is to raise the level of abstraction in requirements engineering, and to work with a look-alike version of the system under development. This enables people who are unfamiliar with LSCs, or who do not want to work with such formal languages directly, to specify the  requirements of systems using a high level, intuitive and user-friendly mechanism. These could include domain experts, application engineers, requirements engineers, and even potential users. What ``play-in" means is that the system's developer first builds the GUI of the system, with no behavior built into it. For GUI-less systems, or for sets of internal objects, we simply use the object model diagram as a GUI. In any case, the user ``plays" the GUI by clicking buttons, rotating knobs and sending messages (calling functions) to hidden objects in an intuitive drag & drop manner. By similarly playing the GUI, the user describes the desired reactions of the system and the conditions that may or must hold. As this is being done, the play-engine continuously constructs LSCs automatically. It queries the application GUI (that was built by the user) for its structure, and interacts with it, thus manipulating the information entered by the user and building and exhibiting the appropriate LSCs.

  • Play-Out : After playing in (a part of) the specification, the natural thing to do is to verify that it reflects what the user intended to say. One way of testing requirements is by constructing a prototype intra-object implementation and using model execution to test it. Instead, we would like to extend the power of our interface-oriented inter-object play methodology, to not only specify the behavior, but to test and validate the requirements as well. And here is where the play-out mechanism enters. In play-out, the user simply plays the GUI application as he/she would have done when executing a system model, or the final system, but limiting him/herself to end-user and external environment actions only. While doing this, the play-engine keeps track of the actions and causes other actions and events to occur as dictated by the universal charts in the specification. Here too, the engine interacts with the GUI application and uses it to reflect the system state at any given moment. This process of the user operating the GUI application and the play-engine causing it to react according to the specification has the effect of working with an executable model, but with no intra-object model having to be built or synthesized. This makes it very easy to let all kinds of people participate in the process of debugging the specification, since they do not need to know anything about the specification or the language used. It yields a specification that is well tested and which has a lower probability of errors in later phases, which are a lot more expensive to detect and eliminate. We should emphasize that the behavior played out need not be the behavior that was played in. The user is not merely tracing scenarios, but is operating the system freely, as he/she sees fit. Universal charts drive the model by their action/reaction nature, whereas existential charts can be used as system tests or as examples of required interactions. Rather than serving to drive the play-out, existential charts are monitored, that is, the Play-Engine simply tracks the events in the chart as they occur. When (and if) a traced chart reaches its end, it is highlighted, and the user is informed that it was successfully traced to completion.

  • Smart Play-Out : Play-out is actually an iterative process, where after each step taken by the user, the Play-Engine computes a super-step, which is a sequence of events carried out by the system as response to the event input by the user. This process is rather naive: for example, there can be many sequences of events possible as a response to a user event, and some of these may not constitute a correct super-step. We consider a super-step to be correct if when it is executed no active universal chart is violated. The multiplicity of possible sequences of reactions to a user event is due to the fact that a declarative inter-object behavior language such as LSCs allows high-level requirements given in pieces (e.g., scenario fragments), leaving open details that may depend on the implementation. The partial order semantics among events in each chart
    and the ability to separate scenarios in different charts without saying explicitly how they should be composed are very useful in early requirement stages, but can cause under-specification and non-determinism when one attempts to execute them. Smart play-out focuses on executing the behavioral requirements with the aid of formal analysis methods, mainly model-checking. Our smart play-out uses model-checking to find a correct super-step if one exists, or proves that there is none. We do this by formulating the play-out task as a verification problem, in such a way that a counterexample resulting from the model-checking will constitute the desired super-step. The transition relation is defined so that it allows progress of active universal charts but prevents violations. The property to be checked is one that states that always at least one of the universal charts is active. In order to falsify it, the model-checker searches for a run in which eventually none of the universal charts is active; i.e., all active universal charts completed successfully, and by the definition of the transition relation no violations occurred. Such a counter-example is exactly the desired super-step. If the model-checker manages to verify the property then no correct super-step exists. The other kind of thing smart play-out can do is to find a way to satisfy an existential chart. Here we cannot limit ourselves to a single super-step, since the chart under scrutiny can contain external events, each of which triggers a super-step of the system. Nevertheless, the formulation as a model-checking problem can be used with slight modifications for this task too. Also, when trying to satisfy an existential LSC, we take the approach that assumes the cooperation of the environment. We should add that the method for satisfying existential LSCs can also be used to verify safety properties that take the form of an assertion on the system state. This is done by putting
    the property's negation in an existential chart and verifying that it cannot be satisfied. 



The Play-Engine has been applied to several case-studies [4] in the OMEGA project: The voting and monitoring subsystem by the Israeli Aircraft Industry (IAI), the MARS model by NLR, and the Depannage telecom service by FTRD.

The GUI used for specifying and executing requirements for the IAI case study is shown below:

  •   IAI Voting and Monitoring GUI

  • A universal chart from the Depannage application by FTRD:

    LSC from Depannage application by FTRD


Several papers and reports are available, containing more info on the Play-Engine and application in Omega.
  • [1]  W. Damm and D. Harel, "LSCs: Breathing Life into Message Sequence Charts", Formal Methods in System Design 19:1 (2001), 45-80.  [PDF, 260Kb]

  • [2]  D. Harel and R. Marelly, "Specifying and Executing Behavioral Requirements: The Play In/Play-Out Approach", Software and System Modeling (SoSyM) 2 (2003), 82-107.  [PDF, 420Kb]
  • [3]  D. Harel, H. Kugler, R. Marelly and A. Pnueli, "Smart Play-Out of Behavioral Requirements", Proc. 4th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2002), November 2002, pp. 378-398. [PDF, 135Kb]
  • [4]  D. Harel, H. Kugler and G. Weiss,  "Some Methodological Observations Resulting from Experience Using LSCs and the Play-In/Play-Out Approach", Proc. Scenarios: Models, Algorithms and Tools, Lecture Notes in Computer Science, Springer-Verlag, 2005 . [PDF]
  • [5] D. Harel and R. Marelly, "Play-Engine User's Guide"  Play-Book

Availability and additional Links

The Play-Engine tool is curently a research prototype tool developed at the Weizmann Institute of Science. For information on availability see the following  Link.

Updates on papers related to the Play-Engine are available through the homepage of Prof. David Harel and the homepage of  Hillel Kugler.


You are currently authenticated as omegapublic (level 0)
For comments about this site please contact the webmaster