St2msc Tool

Description:

Spin trail to a Message Sequence Chart conversion tool (st2msc) was developed as an auxiliary tool to a well-known Spin model checker. If the model of the system does not satisfy the specified requirement, Spin outputs the trail that demonstrates the exact execution path of the system that leads to the wrong behavior. For the real-life systems the Spin trail can be very long and thus very difficult to explore. The st2msc tool converts the Spin trail to a MSC diagram that can be additionally optimized to ease the search for the cause of an error.

Please, send us your questions and comments to: tim.kovse@uni-mb.si.

Screenshots:

Download:

Source: st2msc-src.tar.gz
Binary: st2msc.jar
St2msc Usage:
The program is compiled with Java 1.6.0_07.

Show detected processes in file:
java -jar st2msc.jar -i input.trail -spl

Convert trail file to MSC diagram:
java -jar st2msc.jar -i input.trail -o output.msc

Create virtual process:
java -jar st2msc.jar -i input.trail -o output.msc "1,2,3,4>newProcess"

Rename messages:
java -jar st2msc.jar -i input.trail -o output.msc "1>message1 2>message2 3>message3"

Show help:
java -jar st2msc.jar -h Recent Publications:
T. Kovše - Integration of Spin tool into Development Environment Eclipse (in Slovene) (pdf), 2008
T. Kovše, B. Vlaovič, A. Vreže, and Z. Brezočnik - Spin Trail to a Message Sequence Chart Conversion Tool, ConTEL 2009
T. Kovše, B. Vlaovič, A. Vreže, and Z. Brezočnik - Eclipse Plug-in for Spin and st2msc Tool (pdf), SPIN 2009

Related Tools:

Eclipse Plug-in for Spin