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.
Examples
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:
- A universal chart from the Depannage application by
FTRD:
Resources
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.
|
Home
