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)

PDF Publisher pdf
Language: English


Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (1MB) Preview
[img]
Preview
Official URL
https://doi.org/10.1007/s00165-017-0447-x

Abstract

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

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

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

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

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

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

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

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

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

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: Faculties > Sciences > School of Computing
Depositing User: Peter Welch
Date Deposited: 23 Mar 2018 11:14 UTC
Last Modified: 29 May 2019 20:24 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/66519 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year