LSC was presented by Damm and Harel as a broad extension to the classic Message Sequence Charts (MSC). It captures inter-object communication rigorously in early stage of system development. We believe that LSC is a natural way of specifying system requirements. CSP has long been recognized as a formal language to specify sequential behaviors of a process and synchronization communication between processes with powerful tool supports. In this series of works, we investigate the theoretical relations between LSC and CSP. A large subset of LSC has been formalized using denotaional trace and failure semantics so as to facilitate the semantic transformation from LSCs to CSP. The practical implication of the transformation is threefold.

1. Mature tool support for CSP can be reused to validate LSC specifications. In particular, we use CSP model-checker FDR to establish the consistency of a set of universal charts and the consistency between an existential chart and a set of universal charts. Moreover, we can use FDR to verify important safety and liveness properties by showing there is a refinement relation from the CSP process capturing the properties to the CSP specification constructed from the LSC specification. 

2. We may use well-established CSP algebraic laws to group the local behaviors of each object in the system, so that we may synthesis a set of distributed processes from LSCs automatically. The principle is to use a fixed implementation to avoid undecidability.
3. Existing CSP-based process oriented design packages for concurrency, implemented in Java can be reused to generate executable Java programs all the way from LSC. For this work, we assume that a Java class skeleton of the system is available.

• BNF Grammar for Live Sequence Charts.

• XML Schema Grammar for Live Sequence Charts.

     XML Representation of Example LSCs:

• Deadlock Example: The inconsistency example found in the original journal of LSCs (FMSD, 2001), Figure 10. It is a part of the LSC specification of railway system. 

• Symbolic Example: A part of the LSC specification of a phone system found in the samples of Play Engine tool. Both symbolic instances and messages are found in this example.

• Phone System Example: The full phone system example.

• Event-based Fairness ps

• From Live Sequence Charts to Implementation ps

LSC2CSP Transformation Examples

• Deadlock Example: The inconsistency example found in the original journal of LSC (FMSD, 2001), Figure 10.  The generated machine readable CSP program is here.
• Symbolic Example: A part of the LSC specification of a phone system found in the samples of Play Engine tool. The generated machine readable CSP program is here.
• Phone System Example: The full phone system example. The generated machine readable CSP program is here.
• FDR Verification Screen Capture
• LSC2CSP Rewriting Program

• Rules: Synthesis a set of distributed processes from LSCs, where local behaviors of each object in the system are grouped together. The formal construction and transformation of the CSP processes are documented in here.

• Correctness: A proof of the transformation is here.

• Example: A lift system case study is used as a running example to demonstrate our method. Reasons are that the lift system is a standard example of reactive systems, and people are familiar with the user requirements of a lift system, and the lift system is not a trivial example because of the complexity caused by inherent concurrent interaction in the system. A lift system consists of a lift providing transport between N floors of the building as dictated by the pressing of a range of service-request buttons. Inside the lift there is a panel of buttons, one for requesting travel to each of the building's floors. There are two service-request buttons on each floor, for upward and downward travel respectively, though on the first floor and the top floor there is only one button. Pressing an internal button requests a lift to visit the corresponding floor. Pressing an external button requests a lift to visit the floor with the desired direction of travel. For simplicity, only the following four active components in the lift systems are interested, a Controller that cooperates the lift system, a Shaft through which the controller control the movement of the lift, a Door and a set of Users.

  1. The Lift System Example in LSCs and CSP.

  2. The Lift System Example in XML.

  3. The Lift System Example in Java.

The following experiments have been performed using FDR version 2.78 on a Solaris Unix System with 1G user memory. The measured time is the time taken for verifying the given assertion in the batch mode.

System Description

Assertions

Result

Time Spent

Fig. 10 in (FMSD 2001) fdr

deadlock-free

False

user 0m0.100s
sys 0m0.120s

Above Corrected fdr

Vending Machine (3 U Charts) fdr

Same Above

The phone system specification in Play-Engine, which contains 19  universal charts, a couples of existential charts, local and global variables, symbolic messages. (fdr)

User case: Antenna

 Core user cases

 Phone System Corrected and Simplified (trace preserving).

 Phone System Corrected and Simplified (trace preserving).

The classic dining philosophy example, which contains symbolic instances.

5 Philosophies

8 Philosophies

10 Philosophies

The lift system example above, which contains arrays of variables. fdr

 -

Last updated 31/12/2006.