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