documentation

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

SCStudio user instructions can be downloaded from the official release repository.

Help documentation summarizes main SCStudio features and provides their use cases.

Doxygen documentation demonstrates the SCStudio internal structure. 

Opacity and suggestions for improvements can be discussed in our discussion forum.

To draw MSC and HMSC with LaTeX you can use the msc.sty macro package (old version of msc.sty is available here).

The European Telecommunications Standards Institute (ETSI) provides a guidance and assistance on Making Better Standards.

Conference tool paper:

(please, cite this paper when refering to Sequence Chart Studio - Bibtex item)

Martin Bezděka, Ondřej Bouda, Ľuboš Korenčiak, Matúš Madzin, and Vojtěch Řehák. Sequence Chart Studio. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), pages 148-153. IEEE, 2012. Accessible via DOI link.

Abstract: The Sequence Chart Studio (SCStudio) is a user-friendly drawing and verification tool for Message Sequence Charts (MSC). SCStudio supports several checkers that are able to verify properties such as realizability, time consistency, equivalence checking between two MSC diagrams, etc. Some of them are well known, while others are new or non-trivial extensions of existing ones. The graphical front-end is implemented as a Microsoft Visio add-on, whereas the checkers are platform independent. SCStudio is an open source project that provides an open interface for additional modules.

Refactoring of Sequence Chart Studio:

Ondřej Bouda, Refactoring of Sequence Chart Studio, Master Thesis, Masaryk University, Brno, May 2013. Archived in is.muni.cz.

Abstract: Sequence Chart Studio is a tool for formal modelling and verification of communication protocols specified in Message Sequence Chart. It features a user-friendly graphical user interface and algorithms for checking properties, computing differences between specification and actual flows, rearranging diagrams, and several other functions. All parts have been implemented as students’ work. The tool was initially designed to work with messages as the only type of events on communicating instances, and did not allow to reasonably extend it to support other types of events. The purpose of this work was to refactor the application core to enable further extensions. As a consequence, all the algorithms and other dependent code was to be adjusted without affecting their functionality. A sequence of gradual steps was performed, resulting in the core refactored successfully. The refactoring was proven useful by actually extending Sequence Chart Studio with two new types of events: local actions and conditions. Although the tool pays attention to comply with the Message Sequence Chart recommendation, in case of conditions, the formalism was found to be rather imperfect. An extended syntax and alternative semantics were proposed for conditions. Within the work, application core code was reviewed, the object model was slightly simplified, and memory problems were greatly reduced.

OpenIMS Modelling for Performance Analysis:

Michal Kohut, OpenIMS Modelling for Performance Analysis, Master Thesis, Masaryk University, Brno, May 2013. Archived in is.muni.cz.

Abstract: The main goal of the thesis is to create formal models of Open IP Multimedia Subsystem (IMS) system based on SIP protocol for possible use in performance analysis. In the thesis, modelling will be done in Message Sequence Chart (MSC) formalism to create MSC diagrams that would describe particular communication sequences in Open IMS. Then, logical connection of these MSCs will be formalized in high-level MSC. Next, comparison of model created by MSC with Open IMS will be done and its advantages and disadvantages will be identified. SCStudio application will be used for modelling of MSC diagrams and therefore it will be also evaluated. MSC formalism has exhibited several problems and at last was found insufficient for modelling and analysing of such a complex system as IMS. Therefore modelling in Petri net and Stochastic Coloured Petri Net have been performed. Created models were suitable for performance analysis. SCStudio has proven itself to be a useful tool for MSC modelling.

Generation of MSC Diagrams from Network Traffic:

Viktor Borza, Generation of MSC Diagrams from Network Traffic, Bachelor Thesis, Masaryk University, Brno, May 2013. Archived in is.muni.cz.

Abstract: Message Sequence Chart (MSC) diagrams were designed for modeling of message-based communication between entities in the network. They are used primarily by developing of a new network protocol as a description of design requirements. However, MSC can be as well used for visualization of real traffic captured from a network. One of the applications aimed at work with MSC formalism is Sequence Chart Studio (SCStudio), which is being developed in research centre Institute for Theoretical Computer Science at FI MUNI. The thesis is focused on the problem of generating Message Sequence Chart (MSC) diagrams from PCAP (packet capture) file format. This functionality was integrated into SCStudio as a new feature for importing PCAP files. This paper describes the developing process and behaviour of implemented functionality.

Implementation of LaTeX Export Filter into Sequence Chart Studio:

Adrian Farmadin, Implementation of LaTeX Export Filter into Sequence Chart Studio, Bachelor Thesis, Masaryk University, Brno, May 2013. Archived in is.muni.cz.

Abstract: Sequence Chart Studio (SCStudio) is a user-friendly drawing and verification tool for Message Sequence Charts (MSC).The main task of this thesis is implementing new export filter in SCStudio. New export filter will convert diagrams to LaTeX format using new MSC LaTeX package. Before the implementation of new export filter the MSC LaTeX package first needed to be extended to support all shapes and shapes adjustments. Result document will contain configuration header which allows user easy modify diagrams.

Time relevant layout of MSC:

Tomáš Márton, Time relevant layout of MSC, Bachelor Thesis, Masaryk University, Brno, May 2013. Archived in is.muni.cz.

Abstract: Sequence Chart Studio (SCStudio) is a user friendly drawing and verification tool for Message Sequence Charts (MSC). Currently the aim of SCStudio is to simplify the layout of MSC and to draw it in well-arranged way. This thesis deals with variation of layout with respect to timestamps. It describes possible ways of MSC arranging and implements the most suitable approach. Furthermore SCStudio is enhanced with variation tightening algorithm, that works with absolute time intervals and also proves its correctness.

Revision of layout configuration:

Milan Malota, Layout Configuration for Message Sequence Charts, Bachelor Thesis, Masaryk University, Brno, May 2012. Archived in is.muni.cz.

Abstract: Message Sequence Chart (MSC) is formalism for specification of communication between entities in the system. For drawing and facilitating work with this formalism Sequence Chart Studio (SCStudio) is being developed within the joint project of ANF DATA, spol. s r. o. and the research centre Institute for Theoretical Computer Science (ITI). SCStudio provides several transformers which are changing the diagram in some way. One of those transformers deals with well-arranged diagrams. This thesis addresses problem of well-arranged basic MSC and conflicts which can occur by setting adjustable parameters. Next, a graphical user interface for setting parameters has been revised and improved. In addition, the complexity of implemented algorithm has been described and different method for solution has been provided.

Improvements in time algorithms:

Ľuboš Korenčiak, Effective Algorithms for Time Relation Checking in Message Sequence Charts, Master Thesis, Masaryk University, Brno, May 2011. Archived in is.muni.cz.

Abstract: SCStudio is a user friendly drawing and verification tool for UML Sequence Diagrams and Message Sequence Charts. Currently SCStudio contains inefficient algorithms for working with time relations. These algorithms are based on solving of Temporal Constraint Satisfaction Problem (TCSP). This thesis provides a survey of approaches concerning with effective solving of TCSP. The most suitable approach for SCStudio was selected. Moreover we propose our own optimization and prove its correctness. We integrated both approaches to the tool SCStudio and we demonstrate that it caused dramatic improvement of performance of time algorithms.

The deciding non-local choice problem (not implemented) is improved in:

Martin Chmelík, Realizability of Message Sequence Graphs, Master Thesis, Masaryk University, Brno, May 2011. Archived in is.muni.cz.

 

Abstract: In this work we focus on the realizability problem of Message Sequence Graphs, i.e., the problem whether a given specification is correctly distributable among parallel components. In the general setting, the problem is proved to be undecidable. Therefore, we search for a restricted class of Message Sequence Graphs that admits a realization, but moreover it is decidable whether a given specification is a member of the class. We design a new class of Message Sequence Graph specifications that admits a deadlock free realization by overloading the existing messages with additional bounded control data. We show that the presented class is the largest known class of deadlock free realizable specifications.

Executable pseudocode (not integrated) for new algorithms is introduced in:

Boris Ranto, Writing Graph Algorithms in Executable Pseudocode, Bachelor Thesis, Masaryk University, Brno, May 2011. Archived in is.muni.cz.

Abstract: The aim of this bachelor thesis is to provide the tool that would allow software designer to write pseudocode that is directly executable without additional complexity in terms of pseudocode simplicity. The thesis is aimed to serve as a learning material for software designers that are willing to comply to the suggested notation.

Checker revision in:

Václav Vacek, New Checkers for Sequence Chart Studio, Master Thesis, Masaryk University, Brno, January 2011. Archived in is.muni.cz.

 

Abstract: For the specification of communication between entities, the formalism called Message Sequence Chart is often used. Even though it originates from the telecommunication area, its usage is not limited to it. A team of students at the Faculty of Informatics has been developing an application for drawing and verifying Message Sequence Charts called Sequence Chart Studio (SCStudio). This thesis describes a part of the implementation process: The existing verification algorithm have been revised, corrected and improved and five new verification algorithms have been implemented. In addition, transformation of a MSC-specification to the language of an LTL-model-checking tool (DiVinE) has been enabled. Finally, several new generic functions have been made reusable to simplify further development of SCStudio.

Automatic BMSC layout is studied in:

Zuzana Pekarčíková, Computer Aided Layout of Message Sequence Charts, Bachelor Thesis, Masaryk University, Brno, January 2011. Archived in is.muni.cz.

Abstract: This thesis addresses the problem of drawing well-arranged Basic Message Sequence Chart (BMSC). The problem is completely analysed. The parameters for setting distances between any elements in BMSC are described. Also the parameters for setting the size of these elements are defined. Next, a graphical user interface for setting these parameters is designed. And finally the algorithms for arranging elements in BMSC are introduced.

Time extensions and algorithms are introduced in:

Ľuboš Korenčiak, Time Extension of Message Sequence Chart, Bachelor Thesis, Masaryk University, Brno, May 2009. Archived in is.muni.cz.

Abstract: Message sequence charts (MSC) is a graphical and textual formalism suitable for specifying distributed communication. It consists of the MSC and a High-level MSC (HMSC). The formalism incorporates the possibility of specifying time in designed systems. There arise severe problems regarding timing constraints in MSC, such as computation of minimal network. First attempts to solve the problems using various approaches have been presented.
In this thesis, we analyze different approaches to time extension of MSC. As most suitable appears to be the approach using labeled partially ordered sets. An extension to this approach is provided to handle computation of minimal network in MSC formalism with coregions and constraints in HMSC. Restriction to proper constraint specification is given, which rules out ambiguous and erroneous constraint specifications. Algorithm pseudocodes for checking proper time constraints are provided.

Probabilistic extensions are introduced in:

Martin Křivánek, Probabilistic Extension of Message Sequence Chart, Bachelor Thesis, Masaryk University, Brno, May 2009. Archived in is.muni.cz.

Abstract: Message Sequence Chart (MSC) is an appealing textual and graphical formalism for describing communicating systems. MSCs can be composed into High-level Message Sequence Charts (hMSC) with greater expressiveness. Recently, time and probability properties have been introduced into MSC. We provide a survey of the current work related to MSC extended by probability. We also suggest how to deal with stochastic information in MSC and hMSC and how to compute performance properties of the system.

The deciding non-local choice problem (not implemented) is introduced in:

Martin Chmelík, Deciding Non-local Choice in High-level Message Sequence Charts, Bachelor Thesis, Masaryk University, Brno, May 2009. Archived in is.muni.cz.

Abstract: Non-local choice property in Message Sequence Chart formalism is causing unwanted and unspecified behavior in the implemented system.
This work focuses on detecting non-local choice in High-level Message Sequence Chart specifications. We propose an algorithm that detects non-local choice. We introduce a new approach to deal with non-local choice, by having further assumptions on the system.
The approach cannot be applied in general, but we can algorithmically decide, whether our approach is appliable. Moreover, when we cannot apply our approach, we may advise the designer, what is causing the inapplicableness.

Import from textual ITU-T Z.120 is described in:

Matúš Madzin, Import of MSC Diagrams From the ITU-T Z.120 Text Representation, Bachelor Thesis, Masaryk University, Brno, May 2009. Archived in is.muni.cz.

Abstract: The result of this thesis is a parser which has been developed as part of the SCStudio application. The parser is used to import message sequence chart from a textual le according to the ITU-T standard. Introductions to the message sequence chart and the SCStudio explain why an application such as the SCStudio is important and why message sequence chart helps to save resources and time of a development. This paper describes a design process and actual behaviour of the parser.

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.

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.

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.