dc.contributor.advisor | Butterfield, Andrew | |
dc.contributor.author | Beg, Mirza Muhammad Arshad | |
dc.date.accessioned | 2018-05-16T15:05:06Z | |
dc.date.available | 2018-05-16T15:05:06Z | |
dc.date.issued | 2016 | |
dc.identifier.citation | Mirza Muhammad Arshad Beg, 'Translating from "State-Rich" to "State Poor" process algebras', [thesis], Trinity College (Dublin, Ireland). School of Computer Science & Statistics, 2016 | |
dc.identifier.other | THESIS 11175 | |
dc.identifier.uri | http://hdl.handle.net/2262/82894 | |
dc.description.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. | |
dc.format | 1 volume | |
dc.language.iso | en | |
dc.publisher | Trinity College (Dublin, Ireland). School of Computer Science & Statistics | |
dc.relation.isversionof | http://stella.catalogue.tcd.ie/iii/encore/record/C__Rb16906396 | |
dc.subject | Computer Science, Ph.D. | |
dc.subject | Ph.D. Trinity College Dublin | |
dc.title | Translating from "State-Rich" to "State Poor" process algebras | |
dc.type | thesis | |
dc.contributor.sponsor | Lero Graduate School of Software Engineering (LGSSE) | |
dc.type.supercollection | thesis_dissertations | |
dc.type.supercollection | refereed_publications | |
dc.type.qualificationlevel | Doctoral | |
dc.type.qualificationname | Doctor of Philosophy (Ph.D.) | |
dc.rights.ecaccessrights | openAccess | |
dc.description.note | TARA (Trinity’s Access to Research Archive) has a robust takedown policy. Please contact us if you have any concerns: rssadmin@tcd.ie | |