Skip to content

Department of  Computing

LTSA Eclipse

LTSA Eclipse is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour.

LTSA Eclipse

  • Overview
  • Install
  • Examples
  • Plug-ins
  • Links
A system in LTSA is modelled as a set of interacting finite state machines. The properties required of the system are also modelled as state machines. LTSA performs compositional reachability analysis to exhaustively search for violations of the desired properties. More formally, each component of a specification is described as a Labelled Transition System (LTS), which contains all the states a component may reach and all the transitions it may perform. However, explicit description of an LTS in terms of its states, set of action labels and transition relation is cumbersome for other than small systems. Consequently, LTSA supports a process algebra notation (FSP) for concise description of component behaviour. The tool allows the LTS corresponding to a FSP specification to be viewed graphically.

Please see the installation notes in the Help Guide for details of installing LTSA Eclipse on the Eclipse IDE. Help on using the install manager in Eclipse can be found here.

Note:  The install site for LTSA Eclipse is:

Please see the LTSA Examples page for sample files to use with LTSA Eclipse.

Additional plug-ins may be used in conjunction with LTSA Eclipse to support model-based engineering tasks.

   ADL Support Plug-in (Darwin, XADL etc)
  UML Plug-in (UML Composite Structure Diagrams, Sequence Charts, Activity Diagrams etc)
  WS-Engineer (Model-based Verification of Service Compositions)

Social Bookmarking: