%T JCSProB: Implementing Integrated Formal Specifications in Concurrent Java
%A  Letu Yang,  Michael R. Poppleton
%E  Alistair A. McEwan,  Steve Schneider,  Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X 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.