Symbolic Simulator Engine for Live Sequence Charts (LSCs)

General Description

The is the simulator to symbolically execute and check behavioral requirements specified by Live Sequence Charts (LSC). This simulator searches all legal execution paths. When a violation is detected, the simulator can automatically backtrack and continue searching. It supports symbolic variables, objects/instances and time constraints, so that we can simulate multiple scenarios at one go. For example, several scenarios which only differ from each other in the value of a variable may be executed as a single scenario where the variable value is left uninstantiated. Similarly, we can simulate scenarios with an unbounded number of objects. Technical details about this simulator can be found in paper "Symbolic Execution of Behavioral Requirements".

Implementation Language

This simulator is implemented on top of the ECLiPSe Constraint Logic Programming System. The information for ECLiPSe is available at http://eclipse.crosscoreoptimization.com/. We run the simulator on ECLiPSe 5.7, on top of SunOS 5.8.

How to execute

After loading the engine.pl and the description files for input models into ECLiPSe, you can either type "begin." or "allsolution." to execute the program. With the "begin." command, the simulator tries to find one legal execution path. It will pause whenever such an legal path is found, or all possibilities have been considered. With the "allsolution." command, the simulator tries to find all legal execution paths.

The trace of the legal execution path will be displayed after the simulation finds such a paths. When a violation is detected, the simulator reports the trace of the illegal path, and automatically backtracks to find the illegal one. In other words, our simulator intends to find a possible execution.

The input can be changed by revising the input messages in the "begin" predicate. The format for messages is described below.

Non-trivial Examples

• Car's behaviors of a rail-car system, including departing and arriving (model2.pl). LSC
• Set the phone's number when a user dials a number and then click the Set button (model5.pl). LSC
• Part of the conversation establishment protocol (model4.pl). LSC

Where are the examples we provides from

• model1.pl: the Figure

• model2.pl: the Figure 10 in paper "LSCs: Breathing Life into Message Sequence Charts"

• model3.pl: the Figure 7(a) in paper "Symbolic Execution of Behavioral Requirements"

• model4.pl: the Figure 13 in paper  "Multiple Instances and Symbolic Variables in Executable Sequence Charts"

• model5.pl: the Figure 11 in paper  "Multiple Instances and Symbolic Variables in Executable Sequence Charts"

• model6.pl: the Figure 4 in paper "Symbolic Execution of Behavioral Requirements"

We also attach pictures for these example. For description about these example, please refer to relevant papers.

NOTE: Our LCS charts in model2.pl,model4.pl and model5.pl are NOT exactly the same as the original ones in the papers.

Relevant Data Structure

The data structure of a live copy is [ChartName, MainChart, PreChart, ChartSymbolicInstanctList, ChartVarList, Cut], which describes the name of a chart that the live copy is generated from, the events and control flow for the main chart, the events and control flow for the prechart, which instances are currently represented by this live copy, the state variables of the chart, and next execution point of the copy, respectively.

ChartSymbolicInstanctList= [[Instance1, IntervalList1], [Instance2, IntervalList2], ...], represent the InvervalListN of the InstanceN, in a live copy of a chart. The format of interval list is [[Min1, Max1], [Min2, Max2],....[Min_n]], where [Min1, Max1] represents numbers which are no less than Min1 and less than Max1, and [Min_n] represents number which are no less than Min_n.

Cut= [Temperature, LocationList], where Temperature is the temperature of this cut, and LocationList describes the progress line of each chart during the execution.

The format of the input message is [Type, SenderClass, SenderConstraints, ReceiverClass, ReceiverConstraints, Message, Temperature]. The Type should be either asend or arecv, representing asynchronous sending and receiving, repectively. SenderClass and ReceiverClass are object classes. SenderConstraints and ReceiverConstraints are interval list to specify objects. SenderConstraints and ReceiverConstraints are either [] (representing non-symbolic objects), or interval lists (representing symbolic objects). Note that we ONLY differ non-symbolic and symbolic objects when input and output, and treat non-symbolic objects as special symbolic objects (with interval list=[[0,0]]) during execution. Temperature means whether the message must be received if it is sent.

Download

    simulator.tar.gz

References

• W. Damm, and D. Harel, LSCs: Breathing Life into Message Sequence Charts, Formal Methods in System Design, 19(1):45--80, 2001.

• R. Marelly, D. Harel, and H. Kugler, Multiple Instances and Symbolic Variables in Executable Sequence Charts, In International Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 83--100,2002.

• T. Wang, A. Roychoudhury, R. H.C. Yap, and S.C. Choudhary. Symbolic Execution of Behavioral Requirements, International Symposium on Practical Applications of Declarative Languages (PADL) 2004, LNCS 3057.  The reader may read this paper to familiarize himself/herself with our simulator.

Last Modified:  20,Jan,2004