The symbiosis of concurrency and verification: teaching and case studies

Concurrency is beginning to be accepted as a core knowledge area in the undergraduate CS

curriculum—no longer isolated, for example, as a support mechanism in a module on operating systems or

reserved as an advanced discipline for later study. Formal verification of system properties is often considered a

difficult subject area, requiring significant mathematical knowledge and generally restricted to smaller systems

employing sequential logic only. This paper presents materials, methods and experiences of teaching concurrency

and verification as a unified subject, as early as possible in the curriculum, so that they become fundamental elements

of our software engineering tool kit—to be used together every day as a matter of course. Concurrency and

verification should live in symbiosis. Verification is essential for concurrent systems as testing becomes especially

inadequate in the face of complex non-deterministic (and, therefore, hard to repeat) behaviours. Concurrency

should simplify the expression of most scales and forms of computer system by reflecting the concurrency of the

worlds in which they operate (and, therefore, have to model); simplified expression leads to simplified reasoning

and, hence, verification. Our approach lets these skills be developed without requiring students to be trained in

the underlying formal mathematics. Instead, we build on the work of those who have engineered that necessary

mathematics into the concurrency models we use (CSP, ?-calculus), the model checker (FDR) that lets us explore

and verify those systems, and the programming languages/libraries (occam-?, Go, JCSP, ProcessJ) that let us

design and build efficient executable systems within these models. This paper introduces a workflow methodology

for the development and verification of concurrent systems; it also presents and reflects on two open-ended case

studies, using this workflow, developed at the authors’ two universities. Concerns analysed include safety (don’t do

bad things), liveness (do good things) and low probability deadlock (that testing fails to discover). The necessary

technical background is given to make this paper self-contained and its work simple to reproduce and extend.