@InProceedings{BarrocasOliveira12a,
  title =        "{JC}ircus 2.0: an {E}xtension of an {A}utomatic {T}ranslator from {C}ircus to {J}ava",
  author=        "Barrocas,  S.L.M. and Oliveira,  Marcel",
  editor=        "Welch, Peter H. and Barnes,  Frederick R. M. and Chalmers,  Kevin and Pedersen,  Jan Bækgaard and Sampson,  Adam T.",
  pages =        "15--36",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2012",
  isbn=          "978-0-9565409-5-9",
  year=          "2012",
  month=         "aug",
  abstract=      "The use of formal methods in the development of concurrent
     systems
considerably reduces the complexity of specifying
     their behaviour and
verifying properties that are inherent
     to them. Development, however,
targets the generation of
     executable programs; hence, translating the
final
     specification into a practical programming language
     becomes
imperative. This translation is usually rather
     problematic due to the
high probability of introducing
     errors in manual translations: the
mapping from some of the
     original concepts in the formal concurrency
model into a
     corresponding construct in the programming language
     is
non-trivial. In recent years, there is a growing effort
     in providing
automatic translation from formal
     specifications into programming
languages. One of these
     efforts, JCircus, translates specifications
written in
     Circus (a combination of Z and CSP) into Java programs
     that
use JCSP, a library that implements most of the CSP
     constructs. The
subtle differences between JCSP and Circus
     implementation of
concurrency, however, imposed restrictions
     to the translation strategy
and, consequently, to JCircus.
     In this paper, we extend JCircus by
providing: (1) a new
     optimised translation strategy to multi-way
synchronisation;
     (2) the translation of complex communications, and; (3)
the
     translation of CSP sharing parallel and interleaving. A
     performance
analysis of the resulting code is also in the
     context of this paper and
provides important insights into
     the practical use of our results."
}