Formal Techniques for Distributed Objects, Components, and Systems

Moving block railway systems are the next generation signalling systems currently under development as part of the Shift2Rail European initiative, including autonomous driving technologies. In this paper, we model a suitable abstraction of a moving block signalling system with autonomous driving as a stochastic priced timed game. We then synthesise safe and optimal driving strategies for the model by applying advanced techniques that combine statistical model checking with reinforcement learning as provided by Uppaal Stratego. Hence, we show the applicability of Uppaal Stratego in this concrete case study.

Causal consistent reversibility blends causality and reversibility. For a concurrent system, it says that an action can be undone provided this has no consequences, thereby making it possible to bring the system back to a past consistent state. Time reversibility is considered instead in the performance evaluation field. A continuous-time Markov chain is time reversible if its behavior remains the same when the direction of time is reversed. We try to bridge these two theories by showing the conditions under which both causal consistent reversibility and time reversibility can be achieved in the setting of a stochastic process algebra.

Non-volatile memory (NVM), aka persistent memory, is a new paradigm for memory that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of novel concepts ensuring correctness of concurrent programming abstractions in the face of persistency. So far, this has lead to the design of a number of persistent concurrent data structures, built to satisfy an associated notion of correctness: durable linearizability.

In this paper, we transfer the principle of durable concurrent correctness to the area of software transactional memory (STM). Software transactional memory algorithms allow for concurrent access to shared state. Like linearizability for concurrent data structures, opacity is the established notion of correctness for STMs. First, we provide a novel definition of durable opacity extending opacity to handle crashes and recovery in the context of NVM. Second, we develop a durably opaque version of an existing STM algorithm, namely the Transactional Mutex Lock (TML). Third, we design a proof technique for durable opacity based on refinement between TML and an operational characterisation of durable opacity by adapting the TMS2 specification. Finally, we apply this proof technique to show that the durable version of TML is indeed durably opaque. The correctness proof is mechanized within Isabelle.

We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time– and value–domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

Generating code from networks of timed automata is a well-researched topic with many proposed approaches, which have in common that they not only generate code for the processes in the network, but necessarily generate additional code for a global scheduler which implements the timed automata semantics. For distributed systems without shared memory, this additional component is, in general, undesired.

In this work, we present a new approach to the generation of correct code (without global scheduler) for distributed systems without shared memory yet with (almost) synchronous clocks if the source model does not depend on a global scheduler. We characterise a set of implementable timed automata models and provide a translation to a timed while language. We show that each computation of the generated program has a network computation path with the same observable behaviour.

Neural networks (NN) are taking over ever more decisions thus far taken by humans, even though verifiable system-level guarantees are far out of reach. Neither is the verification technology available, nor is it even understood what a formal, meaningful, extensible, and scalable testbed might look like for such a technology. The present paper is a modest attempt to improve on both the above aspects. We present a family of formal models that contain basic features of automated decision making contexts and which can be extended with further orthogonal features, ultimately encompassing the scope of autonomous driving. Due to the possibility to model random noise in the decision actuation, each model instance induces a Markov decision process (MDP) as verification object. The NN in this context has the duty to actuate (near-optimal) decisions. From the verification perspective, the externally learnt NN serves as a determinizer of the MDP, the result being a Markov chain which as such is amenable to statistical model checking. The combination of a MDP and a NN encoding the action policy is central to what we call “deep statistical model checking” (DSMC). While being a straightforward extension of statistical model checking, it enables to gain deep insight into questions like “how high is the NN-induced safety risk?”, “how good is the NN compared to the optimal policy?” (obtained by model checking the MDP), or “does further training improve the NN?”. We report on an implementation of DSMC inside The Modest Toolset in combination with externally learnt NNs, demonstrating the potential of DSMC on various instances of the model family.

In process algebra, we can express security properties using an equivalence on processes. However, it is not clear which equivalence is the most suitable for the purpose. Indeed, several definitions of some properties are proposed. For example, the definition of privacy is not unique. This situation means that we are not certain how to express an intuitive security notion. Namely, there is a gap between an intuitive security notion and the formulation. Proper formalization is essential for verification, and our purpose is to bridge this gap.

In the case of the applied pi calculus, an outputted message is not explicitly expressed. This feature suggests that trace equivalence appropriately expresses indistinguishability for attackers in the applied pi calculus. By chasing interchanging bound names and scope extrusions, we prove that trace equivalence is a congruence. Therefore, a security property expressed using trace equivalence is preserved by application of contexts.

Moreover, we construct an epistemic logic for the applied pi calculus. We show that its logical equivalence agrees with trace equivalence. It means that trace equivalence is suitable in the presence of a non-adaptive attacker. Besides, we define several security properties to use our epistemic logic.

There are many models of distributed computing, and no unifying mathematical framework for considering them all. One way to sidestep this issue is to start with simple communication and fault models, and use them as building blocks to derive the complex models studied in the field. We thus define operations like union, succession or repetition, which makes it easier to build complex models from simple ones while retaining expressivity.

To formalize this approach, we abstract away the complex models and operations in the Heard-Of model. This model relies on (possibly asynchronous) rounds; sequence of digraphs, one for each round, capture which messages sent at a given round are received before the receiver goes to the next round. A set of sequences, called a heard-of predicate, defines the legal communication behaviors – that is to say, a model of communication. Because the proposed operations behave well with this transformation of operational models into heard-of predicates, we can derive bounds, characterizations, and implementations of the heard-of predicates for the constructions.

Clock-dependent probabilistic timed automata extend classical timed automata with discrete probabilistic choice, where the probabilities are allowed to depend on the exact values of the clocks. Previous work has shown that the quantitative reachability problem for clock-dependent probabilistic timed automata with at least three clocks is undecidable. In this paper, we consider the subclass of clock-dependent probabilistic timed automata that have one clock, that have clock dependencies described by affine functions, and that satisfy an initialisation condition requiring that, at some point between taking edges with non-trivial clock dependencies, the clock must have an integer value. We present an approach for solving in polynomial time quantitative and qualitative reachability problems of such one-clock initialised clock-dependent probabilistic timed automata. Our results are obtained by a transformation to interval Markov decision processes.

The aim of this work is to design a formal framework for consent management in line with EU’s General Data Protection Regulation (GDPR). To make a general solution, we consider a high-level modeling language for distributed service-oriented systems, building on the paradigm of active objects. Our framework provides a general solution for data subjects to observe and change their privacy settings and to be informed about all personal data stored about them. The solution consists of a set of predefined types for privacy related concepts, a formalization of policy compliance, a set of interfaces that forms the basis of interaction with external users for consent management, a set of classes that is used in interaction with the runtime system, and a runtime system enforcing the consented policies.

Threshold guards are a basic primitive of many fault-tolerant algorithms that solve classical problems of distributed computing, such as reliable broadcast, two-phase commit, and consensus. Moreover, threshold guards can be found in recent blockchain algorithms such as Tendermint consensus. In this tutorial, we give an overview of the techniques implemented in Byzantine Model Checker (ByMC). ByMC implements several techniques for automatic verification of threshold-guarded distributed algorithms. These algorithms have the following features: (1) up to t of processes may crash or behave Byzantine; (2) the correct processes count messages and make progress when they receive sufficiently many messages, e.g., at least \(t+1\); (3) the number n of processes in the system is a parameter, as well as t; (4) and the parameters are restricted by a resilience condition, e.g., \(n > 3t\). Traditionally, these algorithms were implemented in distributed systems with up to ten participating processes. Nowadays, they are implemented in distributed systems that involve hundreds or thousands of processes. To make sure that these algorithms are still correct for that scale, it is imperative to verify them for all possible values of the parameters.

This is a tutorial paper on [St]Mungo, a toolchain based on multiparty session types and their connection to typestates for safe distributed programming in Java language.

The StMungo (“Scribble-to-Mungo”) tool is a bridge between multiparty session types and typestates. StMungo translates a communication protocol, namely a sequence of sends and receives of messages, given as a multiparty session type in the Scribble language, into a typestate specification and a Java API skeleton. The generated API skeleton is then further extended with the necessary logic, and finally typechecked by Mungo. The Mungo tool extends Java with (optional) typestate specifications. A typestate is a state machine specifying a Java object protocol, namely the permitted sequence of method calls of that object. Mungo statically typechecks that method calls follow the object’s protocol, as defined by its typestate specification. Finally, if no errors are reported, the code is compiled with javac and run as standard Java code.

In this tutorial paper we give an overview of the stages of the [St]Mungo toolchain, starting from Scribble communication protocols, translating to Java classes with typestates, and finally to typechecking method calls with Mungo. We illustrate the [St]Mungo toolchain via a real-world case study, the HTTP client-server request-response protocol over TCP. During the tutorial session, we will apply [St]Mungo to a range of examples having increasing complexity, with HTTP being one of them.

We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels).