st2msc tool

Update

April, 2014: St2msc tool has been replaced by An Integrated Development Environment for the Spin Model Checker - SpinRCP

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.

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), 2008. [COBISS.SI-ID 12626710, pdf]
• T. Kovše, B. Vlaovič, A. Vreže, and Z. Brezočnik - Spin Trail to a Message Sequence Chart Conversion Tool, ConTEL 2009. [COBISS.SI-ID 11273750, bibtex,pdf]
• T. Kovše, B. Vlaovič, A. Vreže, and Z. Brezočnik - Eclipse Plug-in for Spin and st2msc Tool, SPIN 2009. [COBISS.SI-ID 13289750, bibtex, pdf]