Skip to main content

Behavioural subtyping in process algebra

Briscoe-Smith, C (2000) Behavioural subtyping in process algebra. Doctor of Philosophy (PhD) thesis, University of Kent. (doi:10.22024/UniKent/01.02.86205) (KAR id:86205)

HTML
Language: English
Download (455kB)
[thumbnail of Behavioural_Subtyping_in_Process_Algebra.gz]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
https://doi.org/10.22024/UniKent/01.02.86205

Abstract

Subtyping relations embody a notion of substitutability, and are an important tool in formal methods. The downward simulation relation is well-known and widely used as a subtyping and refinement relation for state-based approaches, but there is no single relation which is widely accepted to be the subtyping relation for the behavioural setting; however, there are several candidate relations. Developments such as the multi-viewpoint specification method of RM-ODP encourage the use of several different formal methods in a single project. Thus, it becomes important to obtain implementations of a single notion of subtyping in several different paradigms. In this thesis, we attempt to find a process algebraic relation which corresponds to the state-based subtyping relation, downward simulation. While trying to achieve this, we define a translation between a state-based notation and a process algebra, and we uncover some of the similarities and differences between these two specification paradigms. In particular, we investigate the meaning of undefined behaviour in each setting. When a state-based specification does not define an operation, the intent is that the system's behaviour is unspecified (not well-defined) if that operation is invoked. In a process algebra with refusals semantics, however, a process is implicitly specified to refuse any action it is not specified to accept, and such a refusal constitutes well-defined behaviour. As part of our translation, we devise a method of representing the unspecified behaviour of the state-based world in a process definition. Finally, we use our translation to prove that the presence of subtyping between a pair of state-based specifications implies reduction between their LOTOS translations, but that the presence of reduction does not imply subtyping. We conclude that reduction itself does not correspond to state-based subtyping, but that any relation which does must be based on a stronger semantics than reduction, such as bisimulation semantics.

Item Type: Thesis (Doctor of Philosophy (PhD))
DOI/Identification number: 10.22024/UniKent/01.02.86205
Additional information: This thesis has been digitised by EThOS, the British Library digitisation service, for purposes of preservation and dissemination. It was uploaded to KAR on 09 February 2021 in order to hold its content and record within University of Kent systems. It is available Open Access using a Creative Commons Attribution, Non-commercial, No Derivatives (https://creativecommons.org/licenses/by-nc-nd/4.0/) licence so that the thesis and its author, can benefit from opportunities for increased readership and citation. This was done in line with University of Kent policies (https://www.kent.ac.uk/is/strategy/docs/Kent%20Open%20Access%20policy.pdf). If you feel that your rights are compromised by open access to this thesis, or if you would like more information about its availability, please contact us at ResearchSupport@kent.ac.uk and we will seriously consider your claim under the terms of our Take-Down Policy (https://www.kent.ac.uk/is/regulations/library/kar-take-down-policy.html).
Uncontrolled keywords: QA 76 Software, computer programming,
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Q Science > QA Mathematics (inc Computing science)
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Mathematics, Statistics and Actuarial Science
SWORD Depositor: SWORD Copy
Depositing User: SWORD Copy
Date Deposited: 29 Oct 2019 16:34 UTC
Last Modified: 10 Dec 2021 15:28 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/86205 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year