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