next up previous

Final Report of the COST-247 Action


MSCtool: Message Sequence Chart Specification and Verification using PROMELA/SPIN

Ignac Lovrek, Damir Jelavic, Martin Pavelic, Enes Dautovic, Emina Filipovic, Kresimir Madunovic

University of Zagreb
Faculty of Electrical Enginering and Computing
Unska 3
HR-10000 Zagreb
Croatia
Tel: +385 1 612 98 02
Fax: +385 1 612 98 32
E-mail: ignac.lovrek@fer.hr

Abstract:

The paper deals with a specification toll based on Message Sequence Chart and Message Sequence Chart verification using PROMELA/SPIN tool set. Basic features of Message Sequence Chart language as well as graphical and textual representation are listed. Message Sequence Chart editor, translator from graphical to textual form and PROMELA code generator as basic components of the MSCtool are described. Simple specification and verification examples are included.

This presentation has been given during the COST-247 2nd International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia, June 18-19, 1997).

COST-247 Working Group(s): 2

Web Links : http://www.hr/zzt/osoblje/Lovrek.html


This Page was prepared by Mark Jorgensen.


Back to the VASY Home page