dc.contributor.advisor | Fleuriot, Jacques | en |
dc.contributor.advisor | Rovatsos, Michael | en |
dc.contributor.author | Papapanagiotou, Petros | en |
dc.date.accessioned | 2016-11-10T10:28:44Z | |
dc.date.available | 2016-11-10T10:28:44Z | |
dc.date.issued | 2014-11-27 | |
dc.identifier.uri | http://hdl.handle.net/1842/17863 | |
dc.description.abstract | Process modelling is a design approach where a system or procedure is decomposed in
a number of abstract, independent, but connected processes, and then recomposed into
a well-defined workflow specification. Research in formal verification, for its part,
and theorem proving in particular, is focused on the rigorous verification of system
properties using logical proof.
This thesis introduces a systematic methodology for process modelling and composition
based on formal verification. Our aim is to augment the numerous benefits of
a workflow based specification, such as modularity, separation of concerns, interoperability
between heterogeneous (including human-based) components, and optimisation,
with the high level of trust provided by formally verified properties, such as
type correctness, systematic resource accounting (including exception handling), and
deadlock-freedom.
More specifically, we focus on bridging the gap between the deeply theoretical proofs-as-processes paradigm and the highly pragmatic tasks of process specification and
composition. To accomplish this, we embed the proofs-as-processes paradigm within
the modern proof assistant HOL Light. This allows the formal, mechanical translation
of Classical Linear Logic (CLL) proofs to p-calculus processes. Our methodology then
relies on the specification of abstract processes in CLL terms and their composition using
CLL inference. A fully diagrammatic interface is used to guide our developed set
of high level, semi-automated reasoning tools, and to perform intuitive composition
actions including sequential, parallel, and conditional composition.
The end result is a p-calculus specification of the constructed workflow, with guarantees
of correctness for the aforementioned properties. We can then apply a visual,
step-by-step simulation of this workflow or perform an automated workflow deployment
as executable code in the programming language Scala.
We apply our methodology to a use-case of a holiday booking web agent and to the
modelling of real-world collaboration patterns in healthcare, thus demonstrating the
capabilities of our framework and its potential use in a variety of scenarios. | en |
dc.contributor.sponsor | Engineering and Physical Sciences Research Council (EPSRC) | en |
dc.language.iso | en | |
dc.publisher | The University of Edinburgh | en |
dc.relation.hasversion | Papapanagiotou, P. and Fleuriot, J. D. (2013). Formal verification of collaboration patterns in healthcare. Behaviour & Information Technology, pages 1-16. | en |
dc.relation.hasversion | Papapanagiotou, P. and Fleuriot, J. (2010). An Isabelle-Like Procedural Mode for HOL Light. In Ferm¨uller, C. and Voronkov, A., editors, Logic for Programming, Artificial Intelligence, and Reasoning, volume 6397 of Lecture Notes in Computer Science, pages 565–580. Springer Berlin Heidelberg. | en |
dc.relation.hasversion | Papapanagiotou, P. and Fleuriot, J. (2011). Formal verification of web services composition using linear logic and the pi-calculus. In Web Services (ECOWS), 2011 Ninth IEEE European Conference on, pages 31–38, Los Alamitos, CA, USA. IEEE Computer Society. | en |
dc.relation.hasversion | Papapanagiotou, P., Fleuriot, J. and Wilson, S. (2012). Diagrammatically-driven formal verification of web-services composition. In Cox, P., Plimmer, B., and Rodgers, P., editors, Diagrammatic Representation and Inference, volume 7352 of Lecture Notes in Computer Science, pages 241-255. Springer Berlin Heidelberg. | en |
dc.relation.hasversion | Papapanagiotou, P., Fleuriot, J., and Grando, A. (2012a). Rigorous process-based modelling of patterns for collaborative work in healthcare teams. In Computer- Based Medical Systems (CBMS), 2012 25th International Symposium on, pages 1–6. IEEE. | en |
dc.subject | formal verification | en |
dc.subject | workflow | en |
dc.subject | process modelling | en |
dc.subject | process composition | en |
dc.title | Formal verification approach to process modelling and composition | en |
dc.type | Thesis or Dissertation | en |
dc.type.qualificationlevel | Doctoral | en |
dc.type.qualificationname | PhD Doctor of Philosophy | en |
dc.rights.embargodate | 2100-12-31 | |
dcterms.accessRights | Restricted Access | en |