Modern software systems are increasingly concurrent, adaptive, and generative, yet our formal methods still focus primarily on describing what systems do rather than why particular behaviours arise. In this talk, I will present ongoing work on a causal calculus for concurrent systems that combines process algebra, modal logic, and intervention-based causality in the style of Halpern and Pearl.

Abstract We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory and provide an efficient method for reasoning about safety properties. We implement our equational theory in DyNetiKAT – a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our tool prototype.

In this paper we discuss the correctness of an ATL-based model transformation from the systems engineering modelling language SysML into Promela, the input language of the SPIN model checker. More precisely, we reduce showing the correctness of the transformation to showing a notion of what we refer to as observational equivalence of the SysML and the generated Promela models, respectively. This paves the way to a proof technique that could be further exploited in order to argue the correctness of model transformations from SysML to various model checkers, based on the observable actions generated by the systems under analysis.

Determining and computing root causes in system failures is a significant issue in science and engineering. In this paper, we introduce a notion of causality for explaining counterexamples in system analysis based on formal models. The counter-examples are produced by checking for hazardous situati ons expressed in the Hennessy-Milner Logic, in the context of Labelled Transition System models. We also introduce CauseJMu, a tool for automatically identifying such causal computations within a system model. CauseJMu relies on encoding causality in terms of an extension of Hennessy-Milner Logic to recursive formulae with data. The encodings enable deciding whether a certain computation is causal or not, using the mCRL2 model checker.

In the concurrency theory, various semantic equivalences on transition systems are based on traces decorated with some additional observations, generally referred to as decorated traces. Using the generalized powerset construction, recently introduced by a subset of the authors (Silva et al.2010 FSTTCS. LIPIcs8 272–283), we give a coalgebraic presentation of decorated trace semantics. The latter include ready, failure, (complete) trace, possible futures, ready trace and failure trace semantics for labelled transition systems, and ready, (maximal) failure and (maximal) trace semantics for generative probabilistic systems. This yields a uniform notion of minimal representatives for the various decorated trace equivalences, in terms of final Moore automata. As a consequence, proofs of decorated trace equivalence can be given by coinduction, using different types of (Moore-) bisimulation (up-to context).