Translating from "State-Rich" to "State Poor" process algebras
Citation:
Mirza Muhammad Arshad Beg, 'Translating from "State-Rich" to "State Poor" process algebras', [thesis], Trinity College (Dublin, Ireland). School of Computer Science & Statistics, 2016Download Item:
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.
Sponsor
Grant Number
Lero Graduate School of Software Engineering (LGSSE)
Author: Beg, Mirza Muhammad Arshad
Sponsor:
Lero Graduate School of Software Engineering (LGSSE)Advisor:
Butterfield, AndrewPublisher:
Trinity College (Dublin, Ireland). School of Computer Science & StatisticsNote:
TARA (Trinity’s Access to Research Archive) has a robust takedown policy. Please contact us if you have any concerns: rssadmin@tcd.ieType of material:
thesisAvailability:
Full text availableMetadata
Show full item recordLicences: