Paper Details

JCircus 2.0: an Extension of an Automatic Translator from Circus to Java

Authors: Barrocas, S.L.M., Oliveira, Marcel

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.

Proceedings:

Communicating Process Architectures 2012, Peter H. Welch, Frederick R. M. Barnes, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson, 2012, pp 15 - 36 published by Open Channel Publishing Ltd., Bicester

Files: Paper (PDF), Slides (PDF)

This record in other formats:

Web page: BibTEX, Refer
Plain text: BibTEX, Refer

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.