Accelerated Verification of Concurrent Systems

Computers are ubiquitous in our daily lives, ranging from the small chip in your debit card to the data centres that form the foundation of the internet. The behaviour of these computers is described by software. Implementing this software correctly, which means that the actual behaviour is equal to the intended behaviour, is notoriously difficult. This is especially true for
concurrent systems where interaction between computers must also be taken into account.A key ingredient to ensure the correctness of software is to specify its
behaviour in a way that can be analysed formally. In our setting we specify this
behaviour as processes using a process algebra. Model checking is a technique
that considers a model of the specification and automatically verifies that the
specified behaviour matches the intended behaviour, which must also be
specified. The behavioural model of a specification is in our case defined by a
state space consisting of all possible states of the system and a transition
relation between states that defines the (nondeterministic) choices in each
state. A major obstacle for the verification of practical systems is the size of
these state spaces. In this dissertation we investigate several ways to tackle this
problem.We identify several issues pertaining to the soundness and performance in
existing antichain-based refinement algorithms and propose new, correct,
antichain-based algorithms. Refinement is a model checking technique that checks
whether the behaviour of one process refines the behaviour of another process.
It is the basis of a stepwise development methodology in which the correctness
of a system can be established by proving, or computing, that a system refines
its specification.We define a decomposition technique to effectively obtain the state space of a
so called monolithic process. A monolithic process is a single recursive
equation with data parameters, which only uses non-determinism, action
prefixing, and recursion. For the decomposition we can show that a composition
of these processes is strongly bisimilar to the monolithic process under a
suitable synchronisation context. Minimising the resulting processes before
determining their composition can be used to derive a state space that is
smaller than the one obtained by a monolithic exploration.

Another model checking technique considers a specification and a property
written in a formal language and decides whether the specification satisfies
this property, which is called the model checking problem. Parity games are a
typical encoding used for this model checking problem. We formalise how to use
on-the-fly solving techniques of parity games can be applied during the
exploration process, and show that this can help to decide the decision problem
more efficiently by terminating early.

Finally, we propose a thread-safe term library that can be used as the basis for
concurrent model checking algorithms, including the previously described ones.
Terms are one of the fundamental data structures used for computing and
therefore are also extensively used in the toolset where our techniques have
been implemented. To this end we define a new efficient multiple-reader/single
write mutual exclusion algorithm that has been shown to be correct used model
checking. Using the new library in an existing state space generation tool, very
substantial speed ups can be obtained.