|Markus Schlütter||Disclaimer||Last modified: 2005-03-03 11:57 UTC|
MOVES: Software Modeling and Verification
|Computer Science / RWTH / I2 / Research / AG / MCS / MSC / Tools / Msc|
MSC ToolsThis page gives an overview of different tools for working with MSCs (Message Sequence Charts). Please feel free to suggest further tools or submit change requests by email to Markus Schlütter or Volker Stolz.
This is a JAVA-Program for JAVA1.2.2. This project is developed by Mesfin Belachew at the Tata Institute of Fundamental Research. It will be enhanced in the future.
COMPUTATION: First a HMSC is created in graphical form. Then the MSC parts of the HMSC are generated in graphical form. The program works intuitively. A simulation of the MSC is possible. Now a verification is made and the user gets implied MSCs, which have to be proved.
INPUT: A MSC or HMSC system specification or an input file in *.gra form. (Standard unknown)
OUTPUT: A MSC or HMSC in *.gra format or a *.strl file. (ESTEREL is also a standard language.)
Further Link: http://cs.oregonstate.edu/~gandhias/projects/MSC.htm
This is a commercial verification tool. It is often used to verify programs for distributed systems. Originally it was built to verify computer chips.
COMPUTATION: Verification of MSCs, HMSCs and other models in the area of distributed systems. A MSC is built in a C program and then linked with a tool to verify it.
INPUT: A MSC or HMSC in *.strl format, which is typically written in the ESTEREL language.
OUTPUT: A C program with different test cases.
This is a commercial tool for creating real-time based systems. It uses the FDL language for creating modules and communication between these modules.
COMPUTATION: The user has to create a scenario in the FDL language and EventStudio creates different documents to show the different cases.
INPUT: A scenario in FDL-Format.
OUTPUT: A HTML-page or a PDF-document, which shows the different scenarios in a graphical MSC form.
The LTSA - MSC Analyser tool for JAVA is an extension of the Labeled Transition System Analyzer (LTSA) that supports synthesis of behaviour models from scenario-based specifications and detection of implied scenarios.
INPUT: A MSC *.msc file in standard format.
OUTPUT: A labeled transition system.
SYSTEM: This version requires JAVA JRE 1.3.0 or later. It runs also
with JAVA 1.2.2.
LoLA (a Low Level Petri Net Analyzer) has been implemented for the validation of reduction techniques for place/transition net reachability graphs. LoLA features symmetric as well as stubborn set based methods. Net symmetries are automatically computed. Stubborn sets are customized to the particular analysis task. LoLA can analyze reachability of a given state or state predicate, boundedness of the net or a place, deadlocks, dead transitions, reversibility, and existence of home states. LoLA can verify formulas of a branching time logic. Additionally, there is a memory-efficient semi-decision procedure for the satisfiability of a given state predicate.
LoLA is a non commercial tool developed by Karsten Schmidt at Humboldt-Universität zu Berlin.
INPUT: A Petri Net, which can be interpreted as a MSC, written in the LoLA language.
OUTPUT: A graph shown as output.
The Estelle Development Toolset has been developed by Institute national des télécommunications Evry, France.
COMPUTATION: This tool needs a scenario of a complete system in
the ESTELLE format.
INPUT: A complete scenario in Estelle format.
OUTPUT: A simulation of the whole scenario with C++ files, some textual information and MSC files.
This is a commercial tool developed by KLOCwork. The company develops software for modeling and verification. It runs as stand alone version or it can be integrated into the Telelogic Tau software.
COMPUTATION: This converter generates from a MSC or a set of HMSCs a standard SDL document. Which can be verified by different other tools.
INPUT: ITU-T Standard message sequence charts (MSC)and high-level message sequence charts (HMSC) based on MSC-92 standard (Z.120).
OUTPUT: ITU-T Standard Specification and Description Language (SDL)based on SDL-96 standard (Z.100)
This is a commercial tool developed by Telelogic. This company is researching in the sector of software development and verification. The software is used for verification of programs and well known companies, who need "correct" programs, use this environment.
COMPUTATION: Telelogic Tau designs, simulates and verifies distributed software.
INPUT: UML diagrams, TTCN files, SDL files or (with KLOCwork MSC to SDL converter) MSCs and HMSCs.
OUTPUT: A simulation of the software.
This is a commercial tool developed by Sandrila Ltd. The company develops Plugins for MS Visio.
COMPUTATION: This is a Plugin for MS Visio to draw MSCs and HMSCs. So you just get the stencils to draw MSCs.
OUTPUT: A MSC or HMSC for MS Visio.
The SITE-tools have been developed at the Humboldt University Berlin. They can be used to develop and analyze components for SDL with different extensions like ASN.1 or IDL. Every tool is a stand alone program. So it is easier to adjust a program, if standards change or a costumer needs other functionalities. This tool gives one of the open SDL-96 grammar and is used also in commercial tools. For compilation this tool needs Kimwutu.
COMPUTATION: SITE consists of tools for
INPUT: Textual representation of a SDL specification.
OUTPUT: C++ or JAVA code for simulation.
SYSTEM: UNIX and LINUX
The QUEuing SDL Tool has been developed at the University of Essen at the Department of Mathematics and Computer Science, Systems Modeling. It is a performance analyzer with an integrated MSC trace generator including time for analysis.
QUEST is a tool that integrates performance evaluation with the SDL-method. Performance characteristics of planned target platforms as well as the workload descriptions may be attached to an SDL system specification. Transient and stationary performance measures like throughput, response time and utilization are evaluated by discrete event simulation. Moreover the functional behavior of a system under additional restrictions imposed by time and resources can be investigated. The name QUEST summarizes the language QSDL, the methodology of its usage, and the tool itself.
INPUT: Textual representation of a SDL specification.
OUTPUT: A performance analysis and a MSC trace including time information.
JADE has been developed at the Department of Computer Science of the Federal University of Minas Gerais. It is a graphical SDL generator which is still under construction.
INPUT: A JAVA object serialization file.
OUTPUT: A file in JAVA object serialization format and CIF files.
This tool has been developed at the University of Lübeck at the Institute for Telematik by Michael Schmitt. It requires ANTLR.
COMPUTATION: ANTLR parser.
INPUT: A textual representation of a SDL-2000 specification (without macros)
This tool has been developed at the University of Lübeck at the Institute for Telematik. It requires ANTLR.
COMPUTATION: ANTLR Parser.
INPUT: A textual representation of a MSC-2000 specification.
OUTPUT: A graphical overview in tree form is shown; parser can be integrated into own projects
(New Version) This commercial tool has been developed by Cinderella ApS in Denmark. The software development tool supports standardized notations like SDL, ASN.1, MSC, and UML for system design, specification and implementation.
COMPUTATION: Cinderella is for designing, implementing, analyzing and simulating software.
ProgGen is a commercial tool developed by SINTEF Telecom and Informatics, Trondheim Norway for automatic code generation. ProgGen is mainly used as an SDL transformation tool. Both "SDL92" and "SDL88" are supported. ProgGen users may also define their own parsers and use ProgGen as a transformation tool for other languages.
COMPUTATION: It generates from a SDL specification a code in different programming languages.
INPUT: A file in SDL/PR format.
OUTPUT: Code for programming languages like C, C++, CHILL, Occam and Java.
TIMe (The Integrated Method) has been developed at SINTEF Telecom and Informatics, Trondheim Norway and is for free.
TIMe is designed for systems that are reactive, concurrent, real-time, distributed, heterogeneous and complex.
COMPUTATION: TIMe is a guide for developing software.
Melba96 has been developed at the Centre for Advanced Technology in Telecommunications (CATT) at the Royal Melbourne Institute of Technology (RMIT).
COMPUTATION: It is a graphical SDL designing tool.
OUTPUT: SDL specification in SDL GR and SDL PR format.
SDL-RT is a proprietary definition based on SDL graphical symbols relying on C for behaviour.
SDL-RT is a:
SiCat has been developed by Siemens AG. But there was no information available. SICAT is free for universities.
DisCo (Distributed Co-operation) is a formal specification method for reactive systems developed at Tampere University of Technology, Finland. It incorporates a specification language, a methodology for developing specifications using the language, and tool support for the methodology.
COMPUTATION: There exists a toolset for DisCo.
INPUT: Specification in DisCo format.
OUTPUT: MSCs as a little overview.
MOCHA is a joint project between the University of California at Berkeley, the University of Pennsylvania, and the State University of New York at Stony Brook; and is funded in part by the Defense Advanced Research Projects Agency, the National Science Foundation, the Microelectronics Advanced Research Corporation and the Semiconductor Research Corporation.MOCHA is available in two versions, cMocha (Version 1.0.1) and jMocha (Version 2.0).
COMPUTATION: MOCHA designs, analyzes and implements software specifications.
OUTPUT: jMOCHA shows traces as MSCs.
UBET, formerly named MSC/POGA, was devolved by Bell Labs and is a free available tool. It consists of two components a MSC editor for creating one MSC and a graph editor for specifying HMSCs.
COMPUTATION: Test Generation
Process Model Generation
Process Model Generation
INPUT: System specification.
VeriSoft was devolved by Bell Labs and is a commercial tool.
VeriSoft is a tool for software developers and testers of concurrent/reactive/real-time systems.
INPUT: A system design.
OUTPUT: Traces in MSC style.
This tool is an upgrade of pico Virtual Machine (pVM) for developing software. It both has been developed by Charis.
INPUT: Software design.
OUTPUT: Capture of inter-actor message-passing, and display using Message Sequence Charts (MSC).
MESA (MSC Editor, Simulator and Analyzer) was originally developed at the University of Waterloo, Canada and is now maintained by the tele research group of the University of Freiburg. In case you would like to receive a copy for research, please send an email: Prof. Stefan Leue
This tool is under design and works only with Solaris.
For a preliminary description of the tool see the technical report "MESA: Support for Scenario-Based Design of Concurrent Systems".
INPUT: Mesa contains a graphical MSC editor. Z.120 can also be parsed.
OUTPUT: static analysis results, Z.120 MSCs, Promela or ROOM code
Further Link: http://tele.informatik.uni-freiburg.de/~leue/msc.html
The LaTeX macro package for drawing Message Sequence Charts was developed at theTechnical University of Eindhoven by Victor Bos and Sjouke Mauw.
This package should be useful to all people that prepare their texts with LaTeX and want draw MSCs in their texts easily. This is not an MSC editor. It simply takes a textual description of an MSC and draws the corresponding MSC.
The current version of the MSC macro package supports the full MSC2000 language.
COMPUTATION: Creates graphical MSCs in LaTeX.
INPUT: Textual representation of an MSC in LaTeX style.
OUTPUT: A graphical representation of an MSC in a *.dvi, *.ps, ... file.
The Use Case Maps Navigator was developed by the Use Case Maps User Group (UCM-UG).
With this tool you can create and edit
Use Case Maps that are always syntactically correct.Furthermore path transformation and connections inside are represented on a hypergraph-based model. And also nested levels of stubs and plugins can be used without binding of plugins to the stubs.
Binding of path elements to components:
Component attributes (type, formal, anchored, fixed, replicated, color, etc.)
The Navigator supports
annotations for agent systems and performance modelling Generation of LQN performance models (Layered Queuing Networks).
COMPUTATION: Takes Use Case Maps and creates different views to analyze them.
INPUT: A Use Case Map in different formats.
OUTPUT: A graphical representation of an MSC, XML, *.ps, *.pdf files, etc.
This tool has been developed at the Chair of Computer Science 2 (here) by Markus Schlütter.It provides the following events:
It does'nt provide timers and coregions.
HMSCs are converted into dotty graphs.
The new functionality is integrated in the tool MSC Execute .
COMPUTATION: Takes a textual representation and generates a LaTeX-file.
INPUT: A MSC in ITU standard notation.
OUTPUT: A graphical representation of an MSC, *.tex, *.ps, *.pdf files, etc.
This is a commercial tool developed by Telelogic. This company is researching in the sector of software development and verification.
COMPUTATION: ObejectGeode is a toolset which designs, simulates and verifies real-time and distributed applications.
INPUT: UML diagrams, SDL files or MSCs.
OUTPUT: C code and test cases.
This tool has been developed by ANDREA informatique. It gives a GUI for designing and editing MSCs and provides the textual and graphical representation of MSCs.
COMPUTATION: Designing and editing MSCs.
INPUT: A MSC
OUTPUT: A graphical and textual representation of an MSC.
This tool has been developed by ANDREA informatique. It gives a GUI for creating test cases using MSCs and provides the textual and graphical representation of MSCs.
COMPUTATION: Takes a textual representation of a MSC and creates a SUT (system under test).
INPUT: A MSC in textual form.
OUTPUT: Different test cases in graphical and textual form.
This tool has been developed by PragmaDev. It is a commercial tool supporting the extended real time concepts of SDL-RT.
COMPUTATION: The tool takes a SDL-RT specification for generating C code and MSC traces to verify this specification.
INPUT: A SDL-RT specification.
OUTPUT: Certain ways to debug and verify the system.
This tool has been developed by Jens Altmann.
This is a commercial tool developed by ezLab. UCS markets the tool. It is inteded for Visual Software Development of communication protocols, real-time, event-driven and embedded systems.
COMPUTATION: ezSDL is a toolset with SDL and MSC Graphical Editors, Simulator/Debugger, C Code generator, Document generator, MSC tracer.
INPUT: SDL and MSC specification, external code may be added.
OUTPUT: C code
This tool has been developed at the Chair of Computer Science 2 (here) by Markus Schlütter.
This tool uses the MSC2000-Parser developed at the ITU-Lübeck for reading a textual representation of a MSC and converts the processes and events into objects. Then from this representation a framework of JAVA code is generated for executing the MSC in the distributed manner given by the standard ITU-T Z.120. External code can be added easily to give actions and other data a more specific meaning.
The functionality of Mu2L is also integrated.
It provides the following events:
It doesn't provide timers and coregions.
COMPUTATION: MSC Execute is a tool for generating executable JAVA code from MSCs. It is useful for implementing MSCs.
INPUT: MSC specification in textual form; External code may be integrated.
OUTPUT: JAVA code
This tool is been developed by LABCOM.
The SDLT is a free SDL compiler for SDL-PR language that generates SDL-GR in PostScript format.
COMPUTATION: The SDLT is a free SDL compiler for SDL-PR language that generates SDL-GR in PostScript format.
INPUT: SDL specification in textual form.