Paper Details

Communicating Process Architectures (CPA)
 Title: JCSProB: Implementing Integrated Formal Specifications in Concurrent Java
 Conference: Communicating Process Architectures 2007
 Authors: Letu Yang, Michael R. Poppleton
Dependable Systems and Software Engineering, Electronics and Computer Science, University of Southampton
 Abstract: The ProB model checker provides tool support for an integrated formal specification approach, combining the classical state-based B language with the eventbased 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. 

BibTeX Entry