Books Online
Not logged in
- Login
Not Signed In
You are here: Skip Navigation Links

Concurrent Systems Engineering Series
Volume 65, 2007
Communicating Process Architectures 2007 - WoTUG-30
Edited by Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter Welch
ISBN 978-1-58603-767-3

JCSProB: Implementing Integrated Formal Specifications in Concurrent Java 67 - 88


Abstract

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.


  Full Text PDF
Navigation
  Home
  Back
  Forward

Article
  Full Text PDF

$20.00 / € 15,00