Verification of message passing concurrent systems

Thesis

This dissertation is concerned with the development of fully-automatic methods of verification, for message-passing based concurrent systems.

In the first part of the thesis we focus on Erlang, a dynamically typed, higher-order functional language with pattern-matching algebraic data types extended with asynchronous message-passing. We define a sound parametric control-flow analysis for Erlang, which we use to bootstrap the construction of an abstract model that we call Actor Communicating System (ACS). ACS are given semantics by means of Vector Addition Systems (VAS), which have rich decidable properties. We exploit VAS model checking algorithms to prove properties of Erlang programs such as unreachability of error states, mutual exclusion, or bounds on mailboxes. To assess the approach empirically, we constructed Soter, a prototype implementation of the verification method, thereby obtaining the first fully-automatic, infinite-state model checker for a core concurrent fragment of Erlang.

The second part of the thesis addresses one of the major sources of imprecision in the ACS abstraction: process identities. To study the problem of algorithmically verifying models where process identities are accurately represented we turn to the π-calculus, a process algebra based around the notion of name and mobility. The full π-calculus is Turing-powerful so we focus on the depth-bounded fragment introduced by Roland Meyer, which enjoys decidability of some verification problems. The main obstacle in using depth-bounded terms as a target abstract model, is that depth-boundedness of arbitrary π-terms is undecidable. We therefore consider the problem of identifying a fragment of depth-bounded π-calculus for which membership is decidable. We define the first such fragment by means of a novel type system for the π-calculus. Typable terms are ensured to be depth-bounded. Both type-checking and type inference are shown to be decidable. The constructions are based on the novel notion of Τ-compatibility, which imposes a hierarchy between names. The type system's main goal is proving that this hierarchy is preserved under reduction, even in the presence of unbounded name creation and mobility.

Authors: D'Osualdo, E

• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: Concurrency
• Subjects: Computer Science