Maybe this website is out of date.
Please visit the current version.
University of Konstanz
Chair for Software Engineering
Prof. Dr. Stefan Leue

Current Projects


MESA   (Message Sequence Chart Editor Simulator Analyzer)

MESA is a graphical CASE tool that supports system design using the Message Sequence Chart (MSC) notation as it has been standardized in ITU-T recommendation Z.120 originally developed at the University of Waterloo and currently maintained by us.


VIP   (A Visual Interface to Promela)

VIP is a platform independant visual editor for the v-Promela language compatible with the model checker SPIN. V-Promela is a visual, object-oriented extension of Promela, targeting the hierarchical modeling of structure and behaviour of concurent reactive, mesasge based systems.


HSF-SPIN   (A Directed Model Checker)

HSF-SPIN is a model checker that applies directed search and other heuristics in order to find errors faster. It provides near-to-optimal error trails and finds errors in state spaces where depth-first search based model checkers fail. HSF-SPIN is thus focussed on error detection and not on correctness verification.


IBOC   (IMCOS Boundedness Checker)

IBOC is a tool that analyzes buffer boundedness for Communicating Finite State Machine based modeling languages such as UML RealTime and Promela, the input language of the SPIN model checker. It estimates a safe bound for each communication buffer once boundedness is proved for a given model. Otherwise, it reports several counterexamples that indicate the potential design errors in the model which lead to unbounded behaviors. IBOC can also perform automated counterexample analyses for Promela models and use the result to improve the precision of the boundedness determination.