|
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) |
|