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!

Samsung TV E Serie – WLAN Stick

In einem älteren Post habe ich beschrieben das man anstelle des Samsung WLAN Stick auch den günstigeren HAMA WLAN Stick verwenden kann. Dies funktioniert jedoch nur für Samsung Fernseher der C-Serie und D-Serie, für die E-Serie TVs von Samsung kann man den HAMA Stick leider nicht benutzen. Eine Übersicht der Samsung Geräte die mit dem HAMA Stick kompatibel sind findet sich hier.

Den original Samsung WIS12ABGNX/XEC WLAN-Dongle für TV
der kompatibel mit allen TV Geräten der E-Serie ist gibt es für unter 30 Euro bei Amazon.

Alternativ kursieren im Netz auch Anleitungen mit denen man den günstigeren Edimax EW-7718Un WLAN Stick so “umprogrammieren” kann das er am Samsung TV funktioniert. Da man hier aber eine Menge Arbeit in kauf nehmen muss und nur 15 Euro spart ist meine Empfehlung den original Stick zu kaufen.

Wer es trotzdem mit dem Edimax Stick versuchen möchte findet hier die Anleitungen (auf Englisch):

Anleitung 1, Anleitung 2

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.

Causality Checking at Microsoft Research

Stefan Leue, my PhD supervisor, recently visited Microsoft Research in Redmond and gave a lecture on the Causality Checking method we currently develop. Causality Checking will make up a large part of my PhD thesis.

video of the lecture is available online here.

Here is the abstract of his talk:

I will introduce Causality Checking, a technique extending model checking designed to establish causalities for safety property violations in system models. Causality Checking is based on counterfactual reasoning. In particular, it is based on an adoption of the Halpern/Pearl Structural Equation Model (SEM) for establishing actual causes. Causality Checking takes advantage of the fact that using a model checker it is fairly easy to compute both “bad” as well as alternate “good” worlds, where a world corresponds to a finite execution sequence.

Based on our adoption of the SEM I will show how causalities can be determined by performing difference computations on the sets of bad and good executions of a model. I will present two approaches how to perform this computation: one based on an explicit enumeration of all bad and good execution traces of a model, and another one based on an on-the-fly algorithm integrated into standard state space search algorithms used in explicit state model checking. I will sketch applications of Causality Checking to systems analysis by considering a number of case studies, including functional and probabilistic models. I will illustrate how the computed causalities can be displayed as fault trees and serve as a basis for system debugging.


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. 

CausCheck : Causality Checking for Complex System Models

I’m currently developing a new method for automated safety analysis of complex systems.
This method is called Causality Checking and allows for the automated generation of fault trees out of system or software architectures in SysML or UML. This post gives an overview of how Causality Checking works.

CausCheck : Causality Checking for Complex System Models

With the increasing complexity of modern safety-critical systems, the need for model based engineering methods that both help in architecting such systems and to asses their safety and correctness becomes increasingly obvious. Due to the size of the systems, traditional techniques like reviews and testing, on the one hand, and manual fault tree analysis or failure mode and effect analysis, on the other hand, can only be applied to limited parts of the system. The main reason for this limitation lies in the vast amount of time and resources that is consumed by manually executing those techniques. In order to be able to asses the correctness and safety of these systems in a comprehensive manner automated or, at least, computer-aided techniques are needed.

Model Checking is an established technique for the automated analysis of system properties. If a model of the system and a formalized property are given to the model checker, it automatically checks whether it can find property violations. In case a safety property is violated, the model checker returns a counterexample, which consists of a system execution trace leading to the property violation. In recent work LeiLeu11LeiLeu11a we have presented the QuantUM approach which allows for automatic translation of system and software architecture models in UML to the input language of the probabilistic model checker PRISM.

The automatic translation of the UML model to PRISM saves time and resources and prevents errors that where frequently introduced in the manual translation process that was previously used. The remaining challenge is the identification of the causes of the property violation and representing this information in a way that it is interpretable on the level of the UML model. The counterexamples that are computed by the model checker help in retracing the system executions leading to the property violation, but they can only be interpreted at the level of the analysis model. While the visualization of the graph structure of a probabilistic counterexample helps to analyze the counterexamples, it is still difficult to compare the thousands of paths in the counterexample with each other and to discern causal factors during fault analysis.

From Counterexamples via Causality to Fault Trees

In order to lift the probabilistic counterexamples generated by the model checker to the level of the UML model, we propose an automatic approach in KunLL11b that computes causality relationships based on a complete set of probabilistic counterexamples and visualizes the computed causality relationships as fault trees. Fault trees are an industrial standard method to document graphically which combination of events can cause a system hazard. The justification for the causalities determined by our method are based on an adoption of the Structural Equation Model of Halpern and Pearl. We illustrate how to use this model in the analysis of computing systems and extend it to account for event orderings as causal factors. We present an over-approximating implementation of the causality tests derived from the extended model.

We demonstrate that our approach improves and facilitates the analysis of safety critical systems. The resulting fault trees are significantly smaller and hence easier to understand than the probabilistic stochastic counterexample, but still contain all information needed to discern the causes for the occurrence of a hazard.

On-The-Fly Causality Checking

The causality computation for probabilistic counterexamples and the mapping of the causality relationships to fault trees helps to understand how the failure of the systems was caused. Experiments in BeeKLLP12 indicate that the computation of the probabilistic counterexamples, on which the causality computation method relies, accounts for the majority of run-time and memory consumption needed for the causality computation.

The main reason for this is that the probability for each execution trace of the counterexample needs to be computed. While the probability of a system fault is of interest, the information which events cause the system failure is more important to the user. Consequently, we extend QuantUM with a translation from UML models to Promela, the input language of the qualitative model checker SPIN, and adapt our causality method to work on counterexamples that were generated using SPIN. This qualitative method scales much better since no probabilities have to be computed. It is, however, still necessary to enumerate and store all counterexample execution traces and all good execution traces in order to compute the causality relationships. We address this issue in LeiLeu12a and LeiLeu12 by extending the causality model to make it applicable to concurrent system models that are specified by transition systems. Furthermore, we propose a causality checking algorithm which can be integrated into a depth-first search or breadth-first search algorithm that is used for the state space exploration during model checking.

Die Logitech K750 Mac Tastatur mit Solarzellen

Logitech K750 Mac Tastatur

Ich liebe mein Apple Wireless Keyboard, aber was mich gelegentlich nervt ist, dass die Batterien oder Akkus immer im ungünstigsten Moment leer sind. Deswegen habe ich mir nun bei Amazon die Logitech K750 Mac Tastatur mit Solarzellen angeschafft. Das Spezielle an dieser Tastatur ist, dass sie ähnlich wie die bekannten Solar-Taschenrechner funktioniert, nur dass sie zusätzlich auch einen integrierten Akku besitzt, so dass man auch bei Dunkelheit laut Logitech bis zu 3 Wochen mit der Tastatur arbeiten kann. Ein weiterer Pluspunkt gegenüber dem Apple Wireless Keyboard ist der integrierte Nummernblock.

Meine Eindrücke

Vom Design her ist die Tastatur sehr ähnlich zu den Mac Keyboards und passt somit sehr gut zu iMac, MacBook Air oder MacBook Pro. In Puncto Bedienung und Haptik steht das Logitech Mac Keyboard der Apple Tastatur auch in nichts nach. Alles in allem eine klare Empfehlung zum Kauf!

Functional Safety Literature / Books (ISO 26262, IEC 61508)

A collection of books discussing functional safety according to IEC61508 and ISO26262.


Design and Safety Assessment of Critical Systems (recommended)

by Marco Bozzano and Adolfo VillafioritaShort Description (source: amazon.com):
Safety-critical systems, by definition those systems whose failure can cause catastrophic results for people, the environment, and the economy, are becoming increasingly complex both in their functionality and their interactions with the environment. Unfortunately, safety assessments are still largely done manually, a time-consuming and error-prone process. The growing complexity of these systems requires an increase in the skill and efficacy of safety engineers and encourages the adoption of formal and standardized techniques. An introduction to the area of design and verification of safety-critical systems, Design and Safety Assessment of Critical Systems focuses on safety assessment using formal methods. Beginning with an introduction to the fundamental concepts of safety and reliability, it illustrates the pivotal issues of design, development, and safety assessment of critical systems. The core of the book covers traditional notations, techniques, and procedures, including Fault Tree Analysis, FMECA, HAZOP, and Event Tree Analysis, and explains in detail how formal methods can be used to realize such procedures. It looks at the development process of safety-critical systems, and highlights influential management and organizational aspects. Finally, it describes verification and validation techniques and new trends in formal methods for safety and concludes with some widely adopted standards for the certification of safety-critical systems. Providing an in-depth and hands-on view of the application of formal techniques to advanced and critical safety assessments in a variety of industrial sectors, such as transportation, avionics and aerospace, and nuclear power, Design and Safety Assessment of Critical Systems allows anyone with a basic background in mathematics or computer science to move confidently into this advanced arena of safety assessment.

Functional Safety

currently not available

The Safety Critical Systems Handbook

Short Description (source: amazon.com):
Electrical, electronic and programmable electronic systems increasingly carry out safety functions to guard workers and the public against injury or death and the environment against pollution. The international functional safety standard IEC 61508 was revised in 2010, and this is the first comprehensive guide available to the revised standard. As functional safety is applicable to many industries, this book will have a wide readership beyond the chemical and process sector, including oil and gas, power generation, nuclear, aircraft, and automotive industries, plus project, instrumentation, design, and control engineers. * The only comprehensive guide to IEC 61508, updated to cover the 2010 amendments, that will ensure engineers are compliant with the latest process safety systems design and operation standards* Helps readers understand the process required to apply safety critical systems standards*

Please note that this is an incomplete literature list of books on functional safety / automotive safety according to ISO 26262 and IEC 61508.


Funktionale Sicherheit

Short Description (source: amazon.de):
Funktionale Sicherheit ist der Teil der Gesamtanlagensicherheit, der von der korrekten Funktion sicherheitsbezogener Systeme zur Risikoreduzierung abhängt. Die bestimmungsgemäßen Funktionen dieser Systeme, die Sicherheitsfunktionen, müssen unter definierten Fehlerbedingungen und mit definierter hoher Wahrscheinlichkeit ausgeführt werden. Mit der relevanten, generischen Norm IEC 61508 fordert eine Norm erstmals einen quantitativen Nachweis für das verbleibende Risiko! Die Normen IEC 61511 (Prozessindustrie), IEC 61513 (Kernkraftwerke) oder IEC 62061 (Maschinenbereich) spezifizieren die Anforderungen für die verschiedenen Anwendungen. Moderne technische Systeme, die sicherheitskritische Prozesse steuern und regeln, werden immer komplexer, weil die Anforderungen immer vielfältiger werden. In diesem Buch werden u. a. die Überwachung oder Steuerung von Fahrzeugen, Zügen und Flugzeugen oder auch von Maschinen, Kraftwerken und chemischen Anlagen sowie im medizinischen oder sonstigen sicherheitskritischen Bereich behandelt. Außerdem werden die Softwareanforderungen an ein System mit funktionaler Sicherheit ausführlich erörtert. Dieses Buch betrachtet die Normen, behandelt Maßnahmen zur Risikobestimmung und Risikoreduzierung, die verschiedenen Sicherheitsstufen (SIL1 bis SIL4), Hardware- und Software-Komponenten sowie entsprechende Modelle, erforderliche mathematische Verfahren, verschiedene Sicherheitssysteme und enthält zahlreiche Anwendungsbeispiele aus verschiedenen Branchen. So bietet es eine wertvolle Unterstützung bei dem Verständnis und der Realisierung sicherer elektrischer, elektronischer und programmierbarer elektronischer Systeme (E/E/PES).

Funktionale Sicherheit in der Praxis

 currently not available

Funktionale Sicherheit nach ISO 26262: Ein Praxisleitfaden zur Umsetzung

Short Description (source: amazon.de):
Dieses Buch behandelt die prozessrelevanten Aspekte des funktionalen Sicherheitsmanagements und insbesondere die Umsetzung der Anforderungen aus der ISO 26262 hinsichtlich der Planungsaktivitäten. In aufeinander aufbauenden, strukturierten Schritten wird gezeigt, wie sicherheitsrelevante Komponenten geplant und welche Prozessanforderungen damit umgesetzt und verfolgt werden. Exemplarisch geschieht dies an einem durchgängigen Praxisbeispiel aus dem Automotive-Bereich, das den passenden Kontext liefert. Im Einzelnen werden erörtert:- Rollen im Sicherheitslebenszyklus
– Konfigurations- und Änderungsmanagement
– ASIL (Automotive Safety Integrity Level)
– Gefährdungs- und Risikoanalyse
– Verifikations- und Validationsplanung
– Produktentwicklung auf Systemebene
– Dokumentation und Arbeitsprodukte
– Reviews
– Qualifizierung von Softwarewerkzeugen
– RetrospektiveErgänzt werden die Ausführungen durch umfangreiche Umsetzungsbeispiele, hilfreiche Vorlagen und praktische Anwendungstipps. Der Leser wird auf diese Weise durch die notwendigen Prozessphasen des Sicherheitslebenszyklus begleitet und erwirbt ein tieferes Verständnis für den Aufbau des funktionalen Sicherheitsmanagements.

Funktionale Sicherheit in der Praxis

 currently not available

Funktionale Sicherheit im Automobil: ISO 26262, Systemengineering auf Basis eines Sicherheitslebenszyklus und bewährten Managementsystemen

Short Description (source: amazon.de):
Die Funktionale Sicherheit (FuSi) im Automobil wurde in der im November 2011 veröffentlichten Norm ISO 26262 erstmalig beschrieben. Um der wachsenden Komplexität der Funktionen im Automobil und auch den steigenden Anforderungen an die interdisziplinären Projektteams gerecht zu werden, mussten hier der Systemengineering-Ansatz sowie die Ansätze bewährter Managementsysteme neu definiert oder entsprechend ergänzt werden. Im vorliegenden Buch wird aufgezeigt, was daraus für den Entwickler resultiert. Darüber hinaus wird aber auch die Art und Weise beschrieben, wie Sicherheitsmechanismen in Hardware und Software realisiert und analysiert werden.
Dargestellt wird der gesamte Prozess der Systementwicklung, beginnend mit den Grundvoraussetzungen im Qualitätsmanagement über das eigentliche Systemengineering bis hin zur Freigabe eines Fahrzeugs und deren Komponenten für den Straßenverkehr. Dabei wird auf notwendige Risikoanalysen, Sicherheitskonzepte und Architekturentwicklung eingegangen. Kapitel zur Produktrealisierung in Mechanik, Elektronik und Software sowie zur anschließenden Testphase ermöglichen es dem Entwickler, die FuSi in der Praxis zu realisieren und alle Normforderungen zu erfüllen.

Bitte beachten Sie, dass dies eine unvolständige Literaturliste zum Thema Funktionale Sicherheit bzw. Automotive Safety nach den Normen IEC 61508 / ISO 26262 ist.

Sharpen the Saw for Computer Scientists

It’s december and a new year will start a few days from now. It’s that time of the year where we think of thinks we want to achieve or do more often the next year. Often theses things include sports, losing weight or spending more time with loved ones.
These are all valid and important new years resolutions and you should go for them. But there is one more thing, let’s think about how we can sharpen our saws to become better at our work. This list is primarily intended for computer scientists and software engineers, developers and architects but probably can be adapted for other professions as well.

Here’s some ideas, some mine, some are inspired by a similar post of Scott Hanselman:

  • Set-aside time, like one or two hours per week, to read technical books or papers related to your field of work.
  • Set-aside time to read one technical paper or book that is not related to your field of work per month.
  • Listen to podcasts, or watch screencasts about new technologies and approaches.
  • Attend conferences and talks and most importantly try to ask questions or at least write down questions and try to figure out the answer for your self.
  • Discuss problems with your co-workers, you might be surprised how much you can learn from a good discussion.
  • Help others, sometimes there is no better and satisfactory way than helping someone to solve a technical problem.
  • Try something new! Whether it is a new programmin language, new software architecting tool or a new software process model you’ll never know when you need it.