Formal analysis of clinical workflow

Recently there has been a growing interest within the field of Health Informatics in applying formal methods to the study, analysis and comparison of medical guidelines. Although there has been no consensus on a standard form for interchange between different languages a number of candidates have been proposed, including the workflow standard defined by the Workflow Management Coalition (WfMC), Process Algebra and Petri Nets (PNs). An attraction of Process Algebra and Petri Nets is that both are formal frameworks which would provide strategies and mechanisms for the formal analysis and comparison of workflow-based languages.

In Grando, Glasspool & Fox (2008) we investigate some advantages of PNs as a standard for the interchange of medical guidelines and as a formal framework for comparing guidelines and guideline languages. In Russell et al. (2006) 43 “prototypical” control flow patterns expressed as Coloured Petri Nets (CPNs) have been proposed to capture in an unambiguous and precise way a wide range of control flow dependencies typically encountered in workflow modeling. While these patterns provide a potential basis for formal and rigorous analysis, they have mainly been used in informal comparative studies of workflow languages and medical guidelines. We have been interested on investigating the possibility of performing similar studies but in a formal way.

Firstly, we present a formal strategy based on simulation equivalence from phi-calculus to prove that a language satisfies a CPN pattern. In more general terms this strategy can be used to prove that two workflows defined in different languages are bisimilar or interchangeable. We argue that this formal strategy contributes to the proposal of using Petri Nets as an standard for the interchange of medical guidelines. In particular we apply this strategy on PROforma by defining an algorithm that maps PROforma plans into Pns, and using the tools available for CPN and concurrent finite-state transition systems.

Secondly, we propose a formal strategy based on analysis by cases to prove that a language does not satisfy a CPN pattern. We argue that close examination of the reasons for the inability of a language to express a particular pattern can provide a principled basis for identifying the language weaknesses and for proposing extensions.

Applying over the Proforma language the proposed formal strategies we obtain different results from the ones presented in Mulyar et al. (2007). Therefore we expect that this approach would provide a more precise study of the expressiveness of PROforma.

Finally, we explain why we think that the prototypical set of patterns of Russell et al. (2006), while covering typical business workflow applications, may not include certain patterns typically found in clinical protocols

References

N. Mulyar, W.M.P. van der Aalst, M. Peleg, A pattern-based analysis of clinical computer-interpretable guideline modeling languages, JAMIA 14(6):781-7, 2007.

N. Russell, A.H.M. ter Hofstede, W.M.P. van der Aalst, and N. Mulyar, Workflow Control-Flow Patterns : A Revised View, BPM Center Report BPM-06-22, 2006.

Publications: Publications related to this work in the COSSAC database.