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.

1st International Conference Automotive Embedded Systems

automotive_embedded_systems

I’m happy to announce that I will chair the 1st International Conference Automotive Embedded Systems. The Automotive Embedded Systems conference focuses on the challenges of nowadays automotive software and systems development.

The conference will be held from 25 – 27 February 2014 at the Lindner Hotel Airport, Düsseldorf, Germany.

We will discuss emerging trends in automotive software and systems engineering such as:

  • model-based engineering,
  • agile development,
  • autonomous driving,
  • safety and security,
  • and many more

I’m looking forward to meet you at the conference!

 

Neues Buch: Funktionale Sicherheit nach ISO 26262

IMG_6836

Ursprünglich hätte das Buch “Funktionale Sicherheit nach ISO 26262: Ein Praxisleitfaden zur Umsetzung” schon in 2012 erscheinen sollen. Mit einiger Verzögerung ist es nun am 31. Juli 2013 erschienen und ist damit aktuell eines der sehr wenigen verfügbaren deutschsprachigen Büchern das sich dem Thema funktionaler Sicherheit nach ISO 26262 widmet.

Kurzbeschreibung (Quelle Amazon):

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
– Retrospektive

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

Ob das Buch hält was es verspricht in kürze hier.

Functional Safety Book recommendation: Design and Safety Assessment of Critical Systems

I have updated my list of literature on functional safety with the book of Marco Bozzano et al..
The book is a very well written introduction into the topic of safety assessment and functional safety and I can recommend it for readers on beginner levels as well as for functional safety experts that want learn more about formal methods and model checking in the context of safety assements.

Design and Safety Assessment of Critical Systems (recommended)

by Marco Bozzano and Adolfo Villafiorita

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

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.

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