Tools
QuantUM: Safety Analysis of Complex Sytem and Software Architectures
When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Also, it is necessary that the description methods used do not require a profound knowledge of formal methods. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. All inputs of the analysis are specified at the level of a UML model. This model is then automatically translated into the analysis model, and the results of the analysis are consequently represented on the level of the UML model. Thus the analysis model and the formal methods used during the analysis are hidden from the user. More ...
DiPro - Directed Probabilistic Counterexample Generation Tool
Current stochastic model checkers do not make counterexamples for property violations readily available. DiPro is a tool, that applies directed explicit state space search to discrete- and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties.
Directed explicit state space search algorithms explore the state space on-the-fly which makes DiPro very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method.
Counterexamples provided by DiPro have two important properties. First, they include those traces which contribute the most amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes.
DiPro allows for the computation of counterexamples for the stochastic model checkers PRISM or MRMC.
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. More ...
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. More ...
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. More ...
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. More ...
