db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
@InProceedings{BarrocasOliveira12a,
title = "{JC}ircus 2.0: an {E}xtension of an {A}utomatic {T}ranslator from {C}ircus to {J}ava",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
author= "Barrocas, S.L.M. and Oliveira, Marcel",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
editor= "Welch, Peter H. and Barnes, Frederick R. M. and Chalmers, Kevin and Pedersen, Jan Bækgaard and Sampson, Adam T.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
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."
}