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