© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Safe and verifiable design of concurrent programs
P.H. Welch, G.H. Hilderink, A.W.P. Bakkers, and G.S. Stiles
In Borko Furht, editor, Proceedings of the 3rd. International Conference on Software Engineering and Applications, pages 182-196. International Association for Science and Technology for Development, October 1999.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.
Bibtex Record
@inproceedings{1018,
author = {P.H. Welch and G.H. Hilderink and A.W.P. Bakkers and G.S. Stiles},
title = {Safe and Verifiable Design of Concurrent Programs},
month = {October},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/1018},
ISBN = {0-88986-273-7},
booktitle = {Proceedings of the 3rd. International Conference on Software Engineering and Applications},
editor = {Borko Furht},
organization = {International Association for Science and Technology for Development},
publication_type = {inproceedings},
refereed = {Yes},
submission_id = {1113_954770552},
}