As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
The ProB model checker provides tool support for an integrated formal specification approach,combiningthe 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 implementationof the combinedB and CSP model has been developedusing 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 reproducethem. Run-time safety and boundedfairness 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.