|
Published: 10th October 2017 DOI: 10.4204/EPTCS.259 ISSN: 2075-2180 |
| Preface Alex Groce and Stefan Leue | |
| On Preemption and Overdetermination in Formal Theories of Causality Sjur K Dyrkolbotn | 1 |
| ACCBench: A Framework for Comparing Causality Algorithms Simon Rehwald, Amjad Ibrahim, Kristian Beckers and Alexander Pretschner | 16 |
| Causality-based Model Checking Bernd Finkbeiner and Andrey Kupriyanov | 31 |
| Causality and Temporal Dependencies in the Design of Fault Management Systems Marco Bozzano | 39 |
| Counterfactual Causality from First Principles? Gregor Gössler, Oleg Sokolsky and Jean-Bernard Stefani | 47 |
| Invited Presentation: Combining Epistemic and Operational Aspects in Compositional Verification of Protocols Mohammad Reza Mousavi | 54 |
| Incorporating Epistemic Uncertainty into the Safety Assurance of Socio-Technical Systems Chris Leong, Tim Kelly and Rob Alexander | 56 |
The second international CREST workshop continued the focus of the first CREST workshop: addressing approaches to causal reasoning in engineering complex embedded and safety-critical systems. Relevant approaches to causal reasoning have been (usually independently) proposed by a variety of communities: AI, concurrency, model-based diagnosis, software engineering, security engineering, and formal methods. The goal of CREST is to bring together researchers and practitioners from these communities to exchange ideas, especially between communities, in order to advance the science of determining root cause(s) for failures of critical systems. The growing complexity of failures such as power grid blackouts, airplane crashes, security and privacy violations, and malfunctioning medical devices or automotive systems makes the goals of CREST more relevant than ever before.
This year’s workshop consisted of two keynotes, three invited presentations, and four contributed papers. The first keynote, presented by Samantha Kleinberg (Stevens Institute of Technology), showed how temporal logic can represent and test rich causal relationships in massive observational datasets. The keynote of Marco Bolzanno (Fondazione Bruno Kessler) proposed a formal approach to fault management for complex systems, including a framework for specification and analysis of diagnosability and the design of fault detection and identification components as well as recent advances in fault propagation analysis. Invited presentations explored causality-based model checking, fault detection and isolation in spacecraft data acquistion systems, and compositional verification of protocols. The contributed papers also covered a variety of topics, including preemption and overdetermination, comparison of causality algorithms, counterfactuals, and epistemic uncertainty.
We wish to thank the keynote speakers and authors of all invited and contributed presentations, who caused the CREST workshop to have its actual substance. The program committee also causally contributed to the successful event, by providing thorough evaluations of the contributions, and useful feedback to authors. The ETAPS organizational committee and chairs of last year’s workshop also produced highly beneficial effects, such as logistical support.
Alex Groce, Northern Arizona University
Stefan Leue, University of Konstanz, Germany
| Georgiana Caltais | University of Konstanz | Germany |
| Hana Chockler | King’s College London | UK |
| Anupam Datta | Carnegie Mellon University | USA |
| Grschwin Fey | University of Bremen | Germany |
| Gregor Goessler | Inria | France |
| Alex Groce | Northern Arizona University | USA (co-chair) |
| Sylvain Hall | Universit du Qubec Chicoutimi | Canada |
| Joseph Halpern | Cornell University | USA |
| Jeff Huang | Texas A&M University | USA |
| Samantha Kleinberg | Stevens Institute of Technology | USA |
| Peter Ladkin | University of Bielefeld | Germany |
| Stefan Leue | University of Konstanz | Germany (co-chair) |
| Peter Lucas | Radboud University Nijmegen | Netherlands |
| Mohammad Reza Mousavi | Halmstad University | Sweden |
| Andy Podgurski | Case Western Reserve University | USA |
| Oleg Sokolsky | University of Pennsylvania | USA |
| Joost Vennekens | K.U. Leuven | Belgium |
| Willem Visser | Stellenbosch University | South Africa |
| Georg Weissenbacher | Vienna University of Technology | Austria |
| Thomas Wies | New York University | USA |
Communication protocols are often described by patterns of actions and interactions; such patterns can be captured by various forms of (communicating) state machines, sequence diagram, or labeled transition systems. Several properties of such protocols such as secrecy, privacy, and authentication are best expressed by notions such as knowledge and belief in epistemic logic or various extensions thereof (5). There have been several proposals to merge these two realms, i.e., the operational realm of protocol specification and the epistemic realm of reasoning. Two significant classes of such approaches are the frameworks based on Dynamic Epistemic Logic (3, 8) and Temporal Epistemic Logic (9), respectively. Some of these frameworks come equipped with mechanized verification tools (4, 15). In (6, 7), we proposed a specification framework based on process algebra furnished with a semantics that allows for verification of properties in a rich logic combining the modal mu-calculus with epistemic logic. Compositional verification for this framework was studied in (1), where the histories of protocols are decomposed into those of their constituent processes.
Another, seemingly different, issue in protocol verification is finding the root causes for a particular violation of a (functional) property. There is a sizeable literature on defining the notion of cause (11, 12, 13, 14), as well as on devising efficient algorithms and tools for finding (minimal) causes (2, 10). In (5), we introduced a notion of causality based on labeled transition systems and Hennessy Milner Logic. There, we also explored some initial ideas regarding the compositionality of calculating causes.
In this talk, we first provide an overview of the above-mentioned two areas. Subsequently, we show how the idea of calculating a cause is similar to checking an epistemic formula: both calculations involve relating different traces leading to a state satisfying a particular property. This leads us to an outline of our approach to decompose causality checking by decomposing the global causality calculation on a parallel composition into local calculations on the constituent processes. We show that finding a minimal cause may still require a calculation at the global (composed process) level; however, this time the calculation can be done on the parallel composition of the projected and reduced processes rather than the original processes. This brings about the potential of reducing the effort in calculating causes.