Trustworthy pervasive healthcare services via multiparty session types

TY - GEN

T1 - Trustworthy pervasive healthcare services via multiparty session types

AU - Henriksen, Anders Starcke

AU - Nielsen, Lasse

AU - Hildebrandt, Thomas

AU - Yoshida, Nobuko

AU - Henglein, Fritz

N1 - Conference code: 2

PY - 2013

Y1 - 2013

N2 - This paper proposes a new theory of multiparty session types extended with propositional assertions and symmetric sum types for modelling collaborative distributed workflows. Multiparty session types statically guarantee that workflows are type-safe and deadlock-free, facilitate automatic generation of participant-specific ("local") workflow protocols from global descriptions, and support flexible implementation of local workflows guaranteed to be compliant with the workflow protocols. The extensions with assertions and symmetric sum types support expressing state-based (pre)conditions and consensual multiparty synchronisation, which are common in complex distributed workflows. We demonstrate the theory's applicability to clinical practice guidelines (CPGs) by providing a prototype implementation targeting mobile healthcare applications. It compiles declarative healthcare workflows specified in a flexible spreadsheet-formatted process matrix into type-checked multiparty processes. The type-checked processes are interpreted on a server communicating with generic, stateless clients running on Android tablet computers, which addresses the pervasiveness requirements common to clinical and home healthcare scenarios. A physician has, with little prior training, successfully used the prototype to design her own healthcare workflow as a process matrix, employing instantaneous test and usage feedback from the prototype.

AB - This paper proposes a new theory of multiparty session types extended with propositional assertions and symmetric sum types for modelling collaborative distributed workflows. Multiparty session types statically guarantee that workflows are type-safe and deadlock-free, facilitate automatic generation of participant-specific ("local") workflow protocols from global descriptions, and support flexible implementation of local workflows guaranteed to be compliant with the workflow protocols. The extensions with assertions and symmetric sum types support expressing state-based (pre)conditions and consensual multiparty synchronisation, which are common in complex distributed workflows. We demonstrate the theory's applicability to clinical practice guidelines (CPGs) by providing a prototype implementation targeting mobile healthcare applications. It compiles declarative healthcare workflows specified in a flexible spreadsheet-formatted process matrix into type-checked multiparty processes. The type-checked processes are interpreted on a server communicating with generic, stateless clients running on Android tablet computers, which addresses the pervasiveness requirements common to clinical and home healthcare scenarios. A physician has, with little prior training, successfully used the prototype to design her own healthcare workflow as a process matrix, employing instantaneous test and usage feedback from the prototype.

U2 - 10.1007/978-3-642-39088-3_8

DO - 10.1007/978-3-642-39088-3_8

M3 - Article in proceedings

SN - 978-3-642-39087-6

T3 - Lecture notes in computer science

SP - 124

EP - 141

BT - Foundations of Health Information Engineering and Systems

A2 - Weber, Jens

A2 - Perseil, Isabelle

PB - Springer

T2 - 2nd International Symposium on Foundations of Health Information Engineering and Systems

Y2 - 27 August 2012 through 28 August 2012

ER -