JACK: A process algebra implementation in Java

Abstract The construction of concurrent programs is especially complex due mainly to the inherent non-determinism of their execution, which makes it di±cult to repeat test scenarios. Concurrency has proved to be a fascinating subject and there are many subtle distinctions which one can make. This dissertation presents an approach for constructing concurrent programs using a set of process algebra constructs (for CSP) implemented as an object-oriented framework in Java called JACK; it stands for Java Architecture with CSP kernel. The main objective of the framework is an implementation of process algebra constructs that provides, as naturally as possible, the algebraic idiom as an extension to this concurrent object-oriented programming language. By naturally, we mean a design and implementation that provide the process abstraction as if it were included in the Java language itself (i.e. embedded in the Java language as an extension package). JACK is a framework that implements a process algebra. A process algebra is a formal language that has notations for describing and reasoning about reactive systems. It implements a modern version of the Hoare's Communication Sequential Process (CSP) formalism. The framework is provided as a Java extension package that supplies CSP operators embedded in the Java language. The library is struc- tured using UML, role modeling for framework design and construction, and make use of design patterns and pattern languages. Furthermore, JACK follows some of the most important software engenieering practices to build frameworks and as a result its design achievies important properties like reusability, simplicity, expres- sive power, modularity, extensibility, and so forth. JACK is provided as a gray-box (white, and black-box) framework tailored to run CSP speci¯cations in Java; it can also be used to model uni¯ed speci¯cations like Circus and CSP-OZ, that combines CSP with Z. The implementation is built using separation of concerns in a way that is highly bene¯cial to class-based design of frameworks. This work empathizes the use of design patterns and pattern languages to properly build frameworks, achieve desired software engineering properties and software quality requirements. The user of the JACK framework is able to describe its process speci¯cation in Java, either in CSP or in a combined algebra one, like in CSP-OZ or in Circus.