Welcome to the JCircus Project Website
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, target 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.
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. We extended JCircus by providing: (1) a new 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 was also in the context of this project and provided important insights into the practical use of our previous results.
In recent years, we verified JCircus. A toolchain that includes a Labelled Predicate Transition System (LPTS) Generator and a Java Pathfinder Model Generator was developed from scratch, in order to allow the verification of the code generated by JCircus, by checking that the input specification is semantically equivalent to the code generated by JCircus. This strategy was applied for an input-set with proper Decision-Coverage criteria.
The contribution of this project was not only extending and verifying JCircus, but also to provide more tools to work with Circus: the LPTS Generator, alongside graphic tools, can provide a better understanding of the behaviour of the specifications in Circus. The LPTS Generator was manually implemented from an updated Operational Semantics for Circus, based on the works of Woodcock, Cavalcanti and Gaudel, whose soundness we proved correct with respect to the Denotational Semantics of Circus (which was another contribution of this project).
On the theoretical level, the strategy we developed for checking the semantic equivalence between Model and Code can be easily adapted to any other Process Algebra (being state-rich or not), and is a good starting point for verifying implementations of more complex state-rich Process Algebras, like OhCircus and SCJ-Circus.
Here you can download some resources related to the project.
Downloads
Source code of JCircus and its toolchain (LPTS Generator + JPF Model Generator)
The source code of JCircus and its toolchain can be downloaded on here.
Outputs of the Verification of JCircus
The outputs of the Verification of JCircus can be downloaded on here.
Coverage Sessions of the Verification of JCircus (EclEmma)
The session files can be downloaded on here.
Proofs of Soundness of the Operational Semantics of Circus
They can be downloaded on here.
Executable
JCircus is now part of the CRefine bundle.
Roulette Example - Input and Output Files
The Circus input specification and the Java generated code can be download from here.
Air Controller Example - Output File
The Java generated code can be download from here.
Verification
The CSP Scripts used to verify the multi-synchronisation solution and the interleaving solution can be download from here.
Experiment - Complex Communication - Input and Output Files
The Circus input specification and the Java generated code can be download from here.
Experiment - Multi-Synchronisation - Input and Output Files
The Circus input specification and the Java generated code can be download from here.
Experiment - Shared Parallel Composition and Interleave - Input and Output Files
The Circus input specification and the Java generated code can be download from here.