Translating from "State-Rich" to "State Poor" process algebras

Abstract

Following the development of formalisms based on data and behavioural aspects of the system, there are a number of attempts in which these two formalisms are mixed together to get benefit of both paradigms. Circus being a living specification language with continuous collaboration from both academia and industry, is a combination of Z, CSP and the refinement calculus. To make use of the available and industry-proven tools for a particular programming paradigm, there is a need to develop a formally verified link between one world and the other. The aim of this work is to develop a formally verified translation between the state-rich process algebra i.e. Circus to the state-poor process algebra i.e. CSP. To achieve the research goal, the most suitable available tools had to be identified. For developing a link between targeted formal languages, the key translations required between the two languages are identified. For ensuring correctness of the translation, the key translation / refinement steps are formalised using a well-known functional language - Haskell. This formed the theoretical core of the work and supported the soundness of the link. In the end, a case study from the collection of software / hardware protocols was selected and the processes specified for the protocol were formally described using the notations available in the prototype designed in Haskell.