Show simple item record

dc.contributor.advisorFleuriot, Jacques
dc.contributor.advisorRovatsos, Michael
dc.contributor.authorPapapanagiotou, Petros
dc.date.accessioned2016-11-10T10:28:44Z
dc.date.available2016-11-10T10:28:44Z
dc.date.issued2014-11-27
dc.identifier.urihttp://hdl.handle.net/1842/17863
dc.description.abstractProcess 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.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.relation.hasversionPapapanagiotou, P. and Fleuriot, J. D. (2013). Formal verification of collaboration patterns in healthcare. Behaviour & Information Technology, pages 1-16.en
dc.relation.hasversionPapapanagiotou, 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.hasversionPapapanagiotou, 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.hasversionPapapanagiotou, 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.hasversionPapapanagiotou, 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.subjectformal verificationen
dc.subjectworkflowen
dc.subjectprocess modellingen
dc.subjectprocess compositionen
dc.titleFormal verification approach to process modelling and compositionen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen
dc.rights.embargodate2100-12-31en
dcterms.accessRightsRestricted Accessen


Files in this item

This item appears in the following Collection(s)

Show simple item record