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)