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 We run the simulator on ECLiPSe 5.7, on top of SunOS 5.8.

How to execute

After loading the 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

Where are the examples we provides from

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

NOTE: Our LCS charts in, and 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.




Last Modified:  20,Jan,2004