Tools
QuantUM: Safety Analysis of Complex Sytem and Software Architectures
Software controls cars, planes, medical equipment, nuclear power plants and many other safety-critical embedded and cyber-physical systems. The malfunctioning of those systems can harm people physically, threaten the environment or cause significant financial losses. When developing such safety-critical systems it is essential to evaluate different design alternatives. Especially in the early design stages a safety assessment of the architectural design is desirable. Manual safety analysis methods (Fault Tree Analysis, FMEA) required by applicable safety standards and industrial best practices are costly and unreliable. 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. At the same time, model–based systems engineering based on UML /SysML architecture models and related design tools (IBM Rhapsody, Enterprise Architect, Artisan Studio, etc.) is an increasingly popular system design approach.
The manufacturers of safety-critical systems and their suppliers need software tools that support automated safety analysis of their system models in order to follow best practices and applicable standards in a cost-effective manner. QuantUM is a tool environment that offers automated model-based functional safety analysis (Fault Tree Analysis, FMEA). It can directly process architecture models edited by the mentioned software design tools. The engineer or developer does not have to be schooled in the use of formal verification methods or tools, yet can use the benefits due to the automatic translation and verification that is done by QuantUM. Results can then be presented in different formats like UML Sequence Diagrams or Fault Trees.
K*: A Heuristic Search Algorithm for Finding the k Shortest Paths
We present a directed search algorithm, called K*, for finding the k shortest paths between a designated pair of vertices in a given directed weighted graph. K* has two advantages compared to current k-shortest-paths algorithms. First, K* operates on-the-fly, which means that it does not require the graph to be explicitly available and stored in main memory. Portions of the graph will be generated as needed. Second, K* can be guided using heuristic functions.
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.
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.