SPIN 2014 Talk: SpinCause: A Tool for Causality Checking

Today I talked at the SPIN 2014 symposium in San Jose, CA about the SpinCause tool. The slides for my talk are available here.

In this paper we present the SpinCause tool for causality checking of Promela and PRISM models. We give an overview of the capabilities of SpinCause and briefly sketch how the causality checking algorithms are integrated into the state-space exploration algorithms used for model checking. In addition we compare the runtime and memory needed for causality checking with the different state-space exploration algorithms and two newly proposed iterative causality checking approaches.

AVM 2013 Talk: Recent Advances in Causality Checking

On Tuesday May 28th 2013 I gave a talk at the Alpine Verification Meeting in Trento Italy with the title “Recent Advances in Causality Checking”. 

Abstract: In recent work on the safety analysis of systems we have shown how causal relationships amongst events can be algorithmically inferred from probabilistic counterexamples and subsequently be mapped to fault trees. The resulting fault trees were significantly smaller and hence easier to understand than the corresponding probabilistic counterexample, but still contain all information needed to discern the causes for the occurrence of a hazard. More recently we have developed an approach called Causality Checking which is integrated into the state-space exploration algorithms used for qualitative model checking and which is capable of computing causality relationships on-the-fly. The causality checking approach outperforms the probabilistic causality computation in terms of run-time and memory consumption, but can not provide a probabilistic measure. In my talk I will give an introduction to causality checking and probabilistic causality computation. Furthermore I will discuss how the strengths of both approaches can be combined to an approach where the causal events are computed using causality checking and the probability computation can be limited to the causal events.

The slides of my talk can be downloaded here.

Speaking at 3rd International Conference Applying ISO 26262

I will be speaking at the 3rd International Conference Applying ISO 26262 on Thursday March, 21 2013. The title of my talk is  “Model-based Engineering and ISO26262” and I will talk about our experiences in using model-based engineering in an ISO 26262 context and lessons learned that we identified. If you are at the conference and are interested in model-based engineering we should talk!

Causality Checking for Complex System Models (Talk at VMCAI 2013)

I gave a talk on causality checking for complex system models at the VMCAI 2013 conference in Rome, Italy.

The slides of my talk are available here.

With the increasing growth of the size and complexity of modern safety-critical systems, the demand for model based engineering methods that both help in architecting such systems and to asses their safety and correctness becomes increasingly obvious. Causality checking is an automated method for formal causality analysis of system models and system execution traces. In this paper we report on work in progress towards an on-the-fly approach for causality checking of system models. We also sketch how this approach can be applied in model-based system analysis when assessing the system’s functional correctness.

Google Scholar Author Profiles

I just discovered a great new (?) feature of Google Scholar called author profiles.

There a two great benefits:

  • You can “follow”  authors and automatically get an email alert whenever they have published a paper, in my opinion a great way to keep track of what is going on in your research field.
  • You can “follow” citations of authors and for instance automatically get an email alert when somebody cites your paper.

A minor but still interesting point is that you can create a public or private author profile where

  • all your publications are listed,
  • metrics like citation count, h-index, i10-index and so on are computed,
  • and you can enter a link to your current website.

My public Google Scholar Author Profile can be found here. 

DiPro – Directed Probabilistic Counterexample Generation Tool Released

After many months of implementation and testing we finally released the DiPro tool for probabilistic counterexample generation tool.
I will give a talk on DiPro’s features on the SPIN 2011 Workshop (July 14-15), co-located with CAV 2011 in Snowbird Utah.

What is DiPro?

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.

Download DiPro here.

Quantitative Safety Analysis of UML Models

My master’s thesis is now available online here.


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. Another obstacle is, that the methods often require a profound knowledge of formal methods, which can rarely be found in industrial practice. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.