WoTUG - The place for concurrent processes

Paper Details


%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.


If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.

Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org

Valid HTML 4.01!