Skip to main content
Kent Academic Repository

Safe and Verifiable Design of Concurrent Programs

Welch, Peter H. and Hilderink, Gerald H. and Bakkers, A.W.P. and Stiles, Gardiner S. (1999) Safe and Verifiable Design of Concurrent Programs. In: Furht, Borko, ed. Proceedings of the 3rd Annual IASTED International Conference Software Engineering and Applications (SEA'99). IASTED/ACTA Press, pp. 20-26. ISBN 0-88986-273-7. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:21756)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.


The design of concurrent programs has a reputation for being difficult, and thus potentially dangerous in safety-critical real-time and embedded systems. The recent appearance of Java, with its simple thread model, and new CASE tools that can verify and check the design of concurrent applications, now significantly reduce design and testing time and eliminate those problems which commonly plague concurrent systems. Our approach uses recently developed Java class libraries based on Hoare's Communicating Sequential Processes (CSP); the use of CSP greatly simplifies the design of concurrent systems and, in many cases, a parallel approach often significantly simplifies systems originally approached sequentially. New CSP CASE tools permit designs to be verified against formal specifications and checked for deadlock and livelock. Below we introduce CSP and its implementation in Java and develop a small concurrent application. The formal CSP description of the application is provided, as well as that of an equivalent sequential version. FDR is used to verify the correctness of both implementations, their equivalence, and their freedom from deadlock and livelock.

Item Type: Book section
Uncontrolled keywords: CSP, JCSP, threads, FDR, safety, deadlock, verifyability, formal design
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 09 Sep 2009 14:36 UTC
Last Modified: 12 Jul 2022 10:39 UTC
Resource URI: (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.