Introduction

Abstract

Distributed, concurrent, and reactive systems, are playing an increasingly important role in computer science, both in theory and in practice. Software systems with these characteristics, among them communication protocols, database systems, and operating systems, tend to exhibit a rich set of behaviours, are inherently complex and therefore complicated to build. Consequently, a great deal of work has been done investigating formal techniques supporting the correct construction of concurrent systems, as well as their verification. The latter is often of particular interest, since concurrent systems are being used in e.g. safety-critical control systems and arise in the design of digital circuits. Verification can then be applied to guarantee that central aspects of the intended system behaviour, like e.g. safety or liveness properties, are correct with respect to their specifications. In contrast to pure testing, this methodology has the important benefit that it directly supports early error detection by revealing logical errors already in the design phase, as well as that it increases considerably the confidence into the correctness of the produced software.