Welcome

 Top Next

Plug-ins for the [image] Case Tool

Help Guide

LTSA Home Page

Distributed Systems Engineering Group, Department of Computing, 180 Queen's Gate, Imperial College London , SW7 2AZ United Kingdom


Introduction

 Top Previous Next

The LTSA Eclipse plug-ins for the SENSORIA Case Tool are a set of services providing interfaces to the LTSA suite of model-checking tools. The SENSORIA Case Tool provides a framework for offering these services and can be used to script the execution of service methods in a workflow style. The set of LTSA services and functions currently available includes the following:

· Core LTSA safety, liveness property model checking
· WS-Engineer (WS-BPEL and WS-CDL) FSP models and property checking
· LTSA MSC (MSC from LTSA traces and from MSC XML)
· LTSA UML (LTSA and FSP models and analysis from UML XMI Models)


Glossary and Acronyms

Acronym | Description
FSP | Finite State Processes
LTSA | The Labelled Transition System Analyser
MSC | Message Sequence Chart


Installation

The LTSA Eclipse SENSORIA Case Tool plug-ins require the LTSA Eclipse plug-in, and can be installed as features from the main LTSA Eclipse Update site (which is used via the Help -> Software Updates -> Find and Install option in the Eclipse IDE.

Please see the LTSA Eclipse help guide for further details of installing the core LTSA Eclipse and associated plug-ins.


Tutorials

Featured tutorials include:

1. Illustrated MSC Trace from the safety check of a BPEL process

2. MSC Trace of a UML Interaction Diagram


MSC Trace from BPEL Process

This tutorial demonstrates producing a Message Sequence Chart trace from the analysis of a Business Process Execution Language for Web Service (BPEL4WS) process specification. Each step is illustrated with an example figure.

1. Locate the SENSORIA Browser view and check that the following plug-ins have been installed.

Analysis -> Web Services -> WS-Engineer

Modeller -> MSC -> LTSA MSC

2. Select and invoke the checkBPELProgress method on the WS-Engineer Tool info view, and then use the invoke function wizard to select a BPEL process file or string.

3. If the call was successful, check that the result is on the SCT Blackboard view.

4. Use the result on the SCT Blackboard as Input to the LTSA MSC plug-in method mscFromLTSATrace.

5. If successful, a new LTSA MSC editor window will display with a graphical trace of the BPEL interactions. If the call is not successful, please check the result on the SCT Blackboard.


MSC Trace of UML Interactions

This tutorial demonstrates producing a Message Sequence Chart trace from the analysis of a UML2 interaction specification (exported to UML XMI 2 standards). Each step is illustrated with an example figure.

Note that this tutorial requires sources files downloaded from here: http://www.doc.ic.ac.uk/ltsa/eclipse/sensoria/tutorials/umlmscexample1.zip

1. Locate the SENSORIA Browser view and check that the following plug-ins have been installed.

Modeller -> MSC -> LTSA MSC

Modeller -> UML -> LTSA UML XMI

2. Select the LTSA UML XMI plug-in and execute the mscXMLFromUMLInteraction service method, using a valid UML2 XMI document containing the UML Interaction.

3. If successful, an XML document will be placed on the Sensoria Blackboard. If the method is not successful, an error message will be placed on the Sensoria Blackboard.

4. Select the LTSA MSC plug-in and execute the openMSCEditorWithMSC service method, using a successful result of the LTSA UML XMI service method in 3.

5. If successful, the LTSA MSC Editor will be opened displaying a trace from the XML document generated in 3. If the method is not successful, an error message will be placed on the Sensoria Blackboard.


Plug-in Reference

These plug-in references refer to specific details about each LTSA SENSORIA plug-in provided.

The plug-ins are categorized by Software Engineering topic. For example, by Analysis plug-ins or by Modelling plug-ins.


Analysis

The Department of Computing, Imperial College London provides the core LTSA model checker in the Analysis services within the SENSORIA browser.


Model Checking


LTSA

ID: ic.doc.sensoria.ltsa

Name: LTSA

Description: Core LTSA Functions plug-in


Info

ID: ic.doc.sensoria.ltsa

Name: LTSA

Description: Core LTSA Functions plug-in


Functions

Analyse

Provides a method to analyse a Finite State Process model.

Input: An FSP model (type: String)

Output: A Trace (type: String)

Safety

Provides a method to safety check a Finite State Process model.

Input: An FSP model (type: String)

Output: A Trace (type: String)

Progress

Provides a method to progress check a Finite State Process model.

Input: An FSP model (type: String)

Output: A Trace (type: String)

Compile

Provides a method to compile an FSP source model to a Finite State Machine.

Input: An FSP model (type: String)

Output: Result of compilation (type: String)


Web Services

Enter topic text here.


WS-Engineer

Enter topic text here.


Modeller

Enter topic text here.


MSC

Enter topic text here.


UML

Enter topic text here.


Appendix