db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>

%T Formal Analysis of Concurrent Java Systems
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
%A Peter H. Welch,  Jeremy M. R. Martin
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
%E Peter H. Welch,  Andr\[`e] W. P. Bakkers
%B Communicating Process Architectures 2000
%X Java threads are synchronised through primitives based upon
   monitor concepts developed in the early 1970s. The semantics
   of Java\[rs]s primitives have only been presented in natural
   language \-\- this paper remedies this with a simple and
   formal CSP model. In view of the difficulties 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 confidence
   boost. Further, automated model\-checking tools can be used
   to root out dangerous states (such as deadlock and
   livelock), find 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 verified. Given the history of
   erroneous implementations of this key primitive, this is a
   considerable relief.