Safe and Verifiable Design of Concurrent Java Programs
Welch, P.H. and Hilderink, G.H. and Bakkers, A.W.P. and Stiles, G.S. (2001) Safe and Verifiable Design of Concurrent Java Programs. International Journal of Computers and Application, 23 (3). pp. 159-165. ISSN 1206-212X
|Abstract:||The design of concurrent programs has a reputation for being difficult, and thus potentially dangerous in safetycritical real-time and embedded systems. The recent appearance of Java, whilst cleaning up many insecure aspects of OO programming endemic in C++, suffers from a deceptively simple threads model that is an insecure variant of ideas that are over 25 years old . Consequently, we cannot directly exploit a range of new CASE tools -- based upon modern developments in parallel computing theory -- that can verify and check the design of concurrent systems for a variety of dangers
such as deadlock and livelock that otherwise plague us during testing and maintenance and, more seriously, cause catastrophic failure in service.
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.
|Copyright:||© 2001 Acta Press|
Electrical Engineering, Mathematics and Computer Science (EEMCS)
|Link to this item:||http://purl.utwente.nl/publications/42319|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page
Metis ID: 201049