Paper Details

@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."
}

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.