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: Proceedings of the 3rd. International Conference on Software Engineering and Applications. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)

Abstract

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: Conference or workshop item (Paper)
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: Faculties > Science Technology and Medical Studies > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 09 Sep 2009 14:36
Last Modified: 18 Jul 2014 09:04
Resource URI: http://kar.kent.ac.uk/id/eprint/21756 (The current URI for this page, for reference purposes)
  • Depositors only (login required):