Abstract
Safety critical systems often consist of many complex processes. Monitoring the behaviour of such processes is critical for enforcing policies, and achieving efficiency and reliability goals. The paper presents a new graphical language for modeling monitors for time constrained workflow processes. To ensure the correctness of a monitor system, we present a model checking approach for verification. We provide an automated data aware translation from a monitor model and its associated workflow to DVE, the input language of the DiVinE model checker, reducing the time and effort required for model checking. We prove the correctness of the translation and give a detailed case study involving LTL properties for a compensable healthcare workflow with time constraints and monitors.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
DiVinE project, http://divine.fi.muni.cz/ (last accessed on November 2010)
Beeri, C., Eyal, A., Milo, T., Pilberg, A.: Query-based monitoring of BPEL business processes. In: Proceedings of the 2007 ACM SIGMOD International Conference on Management of Data, SIGMOD 2007, pp. 1122–1124. ACM, New York (2007)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal — a Tool Suite for Automatic Verification of Real–Time Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Softw. Eng. 17, 259–273 (1991)
Berthomieu, B., Vernadat, F.: Time petri nets analysis with TINA. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, pp. 123–124. IEEE Computer Society, Washington, DC (2006)
Bertolini, C., Liu, Z., Schaf, M., Stolz, V.: Towards a formal integrated model of collaborative healthcare workflows. UNU-IIST Report No. 450 (June 2011)
Broadfield, L., Banerjee, S., Jewers, H., Pollett, A., Simpson, J.: Guidelines for the management of cancer-related pain in adults. Supportive Care Cancer Site Team, Cancer Care Nova Scotia (2005)
Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009)
Kokash, N., Krause, C., de Vink, E.P.: Time and data-aware analysis of graphical service models in Reo. In: Fiadeiro, J.L., Gnesi, S., Maggiolo-Schettini, A. (eds.) SEFM, pp. 125–134. IEEE Computer Society (2010)
Lamport, L.: Real-Time Model Checking Is Really Simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)
Li, J., Zhu, H., Pu, G., He, J.: A formal model for compensable transactions. In: Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems, pp. 64–73. IEEE Computer Society, Washington, DC (2007)
MacCaull, W., Rabbi, F.: NOVA Workflow: A workflow management tool targeting health services delivery. In: International Symposium on Foundations of Health Information Engineering and Systems, FHIES 2011, Johannesburg, South Africa, pp. 74–91 (2011)
Mashiyat, A.S., Rabbi, F., MacCaull, W.: Modeling and Verifying Timed Compensable Workflows and an Application to Health Care. In: Salaün, G., Schätz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 244–259. Springer, Heidelberg (2011)
Moreno, A., Valls, A., Riaño, D.: Palliasys: agent-based proactive monitoring of palliative patients. In: IWPAAMS (2005)
Muehlen, M.Z., Rosemann, M.: Workflow-based process monitoring and controlling - technical and organizational issues. In: Proceedings of the 33rd Hawaii International Conference on System Science (HICSS-33), pp. 1–10. IEEE Computer Society Press (2000)
Rabbi, F., Wang, H., MacCaull, W.: Compensable WorkFlow Nets. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 122–137. Springer, Heidelberg (2010)
Simmonds, J., Ben-David, S., Chechik, M.: Guided recovery for web service applications. In: Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2010, pp. 247–256. ACM, New York (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rabbi, F., Mashiyat, A.S., MacCaull, W. (2012). Model Checking Workflow Monitors and Its Application to a Pain Management Process. In: Liu, Z., Wassyng, A. (eds) Foundations of Health Informatics Engineering and Systems. FHIES 2011. Lecture Notes in Computer Science, vol 7151. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32355-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-32355-3_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32354-6
Online ISBN: 978-3-642-32355-3
eBook Packages: Computer ScienceComputer Science (R0)