Fleuriot, Jacques

Rovatsos, Michael

Papapanagiotou, Petros

Engineering and Physical Sciences Research Council (EPSRC)

2016-11-10T10:28:44Z

2016-11-10T10:28:44Z

2014-11-27

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.

http://hdl.handle.net/1842/17863

en

The University of Edinburgh

Papapanagiotou, P. and Fleuriot, J. D. (2013). Formal verification of collaboration patterns in healthcare. Behaviour & Information Technology, pages 1-16.

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.

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.

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.

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.

formal verification

workflow

process modelling

process composition

Formal verification approach to process modelling and composition

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy