White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Angelic Processes

De Oliveira Salazar Ribeiro, Pedro Fernando (2014) Angelic Processes. PhD thesis, University of York.

Text (Angelic Processes)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (2149Kb) | Preview


In the formal modelling of systems, demonic and angelic nondeterminism play fundamental roles as abstraction mechanisms. The angelic nature of a choice pertains to the property of avoiding failure whenever possible. As a concept, angelic choice first appeared in automata theory and Turing machines, where it can be implemented via backtracking. It has traditionally been studied in the refinement calculus, and has proved to be useful in a variety of applications and refinement techniques. Recently it has been studied within relational, multirelational and higher-order models. It has been employed for modelling user interactions, game-like scenarios, theorem proving tactics, constraint satisfaction problems and control systems. When the formal modelling of state-rich reactive systems is considered, it only seems natural that both types of nondeterministic choice should be considered. However, despite several treatments of angelic nondeterminism in the context of process algebras, namely Communicating Sequential Processes, the counterpart to the angelic choice of the refinement calculus has been elusive. In this thesis, we develop a semantics in the relational setting of Hoare and He's Unifying Theories of Programming that enables the characterisation of angelic nondeterminism in CSP. Since CSP processes are given semantics in the UTP via designs, that is, pre and postcondition pairs, we first introduce a theory of angelic designs, and an isomorphic multirelational model, that is suitable for characterising processes. We then develop a theory of reactive angelic designs by enforcing the healthiness conditions of CSP. Finally, by introducing a notion of divergence that can undo the history of events, we obtain a model where angelic choice avoids divergence. This lays the foundation for a process algebra with both nondeterministic constructs, where existing and novel abstract modelling approaches can be considered. The UTP basis of our work makes it applicable in the wider context of reactive systems.

Item Type: Thesis (PhD)
Keywords: semantics, formal specification, software engineering, CSP, UTP
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.647072
Depositing User: Mr Pedro Fernando De Oliveira Salazar Ribeiro
Date Deposited: 28 May 2015 11:09
Last Modified: 08 Sep 2016 13:32
URI: http://etheses.whiterose.ac.uk/id/eprint/9020

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)