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

Observation-enhanced verification of operational processes

Paterson, Colin (2018) Observation-enhanced verification of operational processes. PhD thesis, University of York.

This is the latest version of this item.

Thesis-WR.pdf - Examined Thesis (PDF)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (3113Kb) | Preview


Operational processes are at the core of many organisations. The failure and misuse of these processes can cause significant economic losses to businesses or, in the worst cases, endanger human life. As a result, there has been significant research effort focused on the development of techniques and tools for the model-based analysis and verification of reliability, performance and quality-of-service properties of processes. Constructing models which accurately represent the behaviour of real-world systems is very challenging. The complexity and stochastic nature of real-world phenomena requires the use of modelling assumptions which introduce errors that can significantly impact the results of model-based analysis. Where inaccurate analyses are used as the basis of engineering or business decisions, the consequences can be catastrophic. Many operational processes are now routinely instrumented and capture information about component interactions and the behaviour of human operators. This thesis introduces a set of tool-supported techniques which exploit these logs in conjunction with tried and tested probabilistic model checking. This produces Markov models and formal analysis techniques which more accurately capture process behaviours and improve the quality of model-based analysis for operational processes. We show how observation data can be used to improve the modelling and analysis of continuous time systems by refining continuous-time Markov models (CTMCs) to more accurately reflect real-world behaviours. We apply the tools and techniques developed to real-world processes and demonstrate how we may avoid the invalid decisions which arise from traditional CTMC modelling and analysis techniques. We also show how observation-enhanced discrete time Markov models may be used to characterise the behaviour of users within an operational process. The self-adaptive role based access control approach we develop uses a formal definition of adaptation policies to identify potential threats in a real-world IT support system and mitigates risks to the system.

Item Type: Thesis (PhD)
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.770297
Depositing User: Dr Colin Paterson
Date Deposited: 25 Mar 2019 12:25
Last Modified: 19 Feb 2020 13:08
URI: http://etheses.whiterose.ac.uk/id/eprint/23257

Available Versions of this Item

  • Observation-enhanced verification of operational processes. (deposited 25 Mar 2019 12:25) [Currently Displayed]

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)