Skip to main content

The symbiosis of concurrency and verification: teaching and case studies

Pedersen, Jan B., Welch, Peter H. (2017) The symbiosis of concurrency and verification: teaching and case studies. Formal Aspects of Computing, 30 (2). pp. 239-277. ISSN 0934-5043. (doi:10.1007/s00165-017-0447-x) (KAR id:66519)

Abstract

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.

Item Type: Article
DOI/Identification number: 10.1007/s00165-017-0447-x
Uncontrolled keywords: Process-orientation, Concurrency, Deadlock, Event ordering, Liveness, Verification, Occam-?, CSP
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Peter Welch
Date Deposited: 23 Mar 2018 11:14 UTC
Last Modified: 16 Feb 2021 13:53 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/66519 (The current URI for this page, for reference purposes)

University of Kent Author Information

Welch, Peter H..

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.