Documentation

User Instructions can be downloaded from the official release repository.

Data structures and basic algorithms are described in: Jindřich Babica, Message Sequence Charts; Properties And Checking Algorithms, Master Thesis, Masaryk University, Brno, January 2009. Archived in is.muni.cz.

Abstract: Message Sequence Chart (MSC) is a widely used formalism for description of telecommunication systems. A lack of tools to support MSC led us to start development of a new tool -- Sequence Chart Studio (SCStudio). Using this tool one should be capable to design a system in the MSC notation, moreover, the tool will provide automatic checks of several properties of the system. The aim of this thesis was to study MSC and according to its notation set up basis for the SCStudio. We have designed a data structures of MSC, provided functions for their processing and defined several basic properties of MSC. We also implemented checking algorithms for these properties and trace race condition property introduced in separate paper.

The race condition problem is introduced in: Petr Slovák, Race Conditions in Message Sequence Charts, Bachelor Thesis, Masaryk University, Brno, May 2008. Archived in is.muni.cz.

Abstract: Race condition problem is known to be decidable for Message Sequence Charts (MSC) but it becomes undecidable for High-level MSC. This thesis introduces a modification of the race condition problem, so called trace race condition problem, that remains decidable even for High-level MSC (with coregions). In this thesis, we discuss differences between the race condition and the trace race condition problem and we argue that our concept is useful in model based design. We also propose an algorithm solving the trace race condition problem as well as show the problem itself to be NP-complete for HMSC with coregions.

Message Sequence Charts are further described in a research report Formalisms and Tools for Design and Specification of Network Protocols, FIMU-RS-2007-02, Masaryk University, Brno, May 2007.
By Jindřich Babica, Vojtěch Řehák, Petr Slovák, Pavel Troubil, Martin Zavadil.

Abstract: Message Sequence Charts (MSC) are a useful formalism for formalization of network protocols early in their design phase. In this paper, we introduce the basics of MSC language and describe some of the possibilities for automatic location of "problematic" parts in the design. Focus is then given to different modifications of MSC design (FIFO behavior, bounded channels, etc.) as well as formal checking of more complex design properties (MSC membership, realizability). Next, an introduction of Specification and Description Language (SDL) is presented. Possibilities of automatic synthesis of system design in MSC to an SDL model and it's correctness verification are mentioned.

Both MSC and HMSC are standartized in ITU-T Z.120.

The ETSI provides a guidance and assistance on Making Better Standards.

To draw MSC and HMSC with LaTeX you can use the msc.sty macro package.

Doxygen documentation of the main internal structure (msc.h) and the checking algorithms can be found here.