@InProceedings{YangPoppleton07,
  title =        "{JCSP}ro{B}: {I}mplementing {I}ntegrated {F}ormal {S}pecifications in {C}oncurrent {J}ava",
  author=        "Yang,  Letu and Poppleton,  Michael R.",
  editor=        "McEwan,  Alistair A. and Schneider,  Steve and Ifill,  Wilson and Welch, Peter H.",
  pages =        "67--88",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn=          "978-1-58603-767-3",
  year=          "2007",
  month=         "jul",
  abstract=      "The ProB model checker provides tool support for an
     integrated formal
specification approach, combining the
     classical state-based B language with the event based
     process algebra CSP. In this paper, we present a developing
     strategy for implementing such a combined ProB specification
     as a concurrent Java program. A Java implementation of the
     combined B and CSP model has been developed using a similar
     approach to JCSP. A set of translation rules relates the
     formal model to its Java implementation, and we also provide
     a translation tool JCSProB to automatically generate a Java
     program from a ProB specification. To demonstrate and
     exercise the tool, several B/CSP models, varying both in
     syntactic structure and behavioural/concurrency properties,
     are translated by the tool. The models manifest the presence
     and absence of various safety, deadlock, and bounded
     fairness properties; the generated Java code is shown to
     faithfully reproduce them. Run-time safety and bounded
     fairness checking is also demonstrated. The Java programs
     are discussed to demonstrate our implementation of the
     abstract B/CSP concurrencymodel in Java. In conclusion we
     consider the effectiveness and generality of the
     implementation strategy."
}