Skip to main content

Formal Analysis of Concurrent Java Systems

Welch, Peter H. and Martin, Jeremy M. R. (2000) Formal Analysis of Concurrent Java Systems. In: Welch, Peter H. and Bakkers, A.W.P., eds. Communicating Process Architectures 2000. Concurrent Systems Engineering . IOS Press, Amsterdam, Netherlands, pp. 275-301. ISBN 978-1-58603-077-3. (KAR id:21982)

PDF
Language: English
Download (681kB) Preview
[thumbnail of Formal_Analysis_of_Concurrent_Java_Systems.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format

Abstract

Java threads are synchronised through primitives based upon monitor concepts developed in the early 1970s. The semantics of Java's primitives have only been presented in natural language ? this paper remedies this with a simple and formal CSP model. In view of the dif?culties encountered in reasoning about any non-trivial interactions between Java threads, being able to perform that reasoning in a formal context (where careless errors can be highlighted by mechanical checks) should be a considerable con?dence boost. Further, automated model-checking tools can be used to root out dangerous states (such as deadlock and livelock), ?nd overlooked race hazards and prove equivalence between algorithms (e.g. between optimised and unoptimised

versions). A case study using the CSP model to prove the correctness of the JCSP and CTJ channel implementations (which are built using standard Java monitor synchronisation)

is presented. In addition, the JCSP mechanism for ALTing (i.e. waiting for and, then, choosing between multiple events) is veri?ed. Given the history of erroneous implementations of this key primitive, this is a considerable relief.

Item Type: Book section
Uncontrolled keywords: Java, threads, monitors, CSP, JCSP, CTJ, formal verification
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: 12 Sep 2009 19:16 UTC
Last Modified: 12 Jul 2022 10:39 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21982 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year