A Computational Model for The Access to Medical Service in a Basic Prototype of a Healthcare System

• Autorzy: Petre Luigia , Sanwal Usman , Shah Gohar , Panchal Charmi , Tyagi Dwitiya , Petre Ion

Identyfikatory

DOI

10.3233/FI-2020-1886

• Języki publikacji: EN

Abstrakty

EN

How robust is a healthcare system? How does a patient navigate the system and what is the cost (e.g., number of medical services required or number of times the medical provider had to be changed to get access to the required medical services) incurred from the first symptoms to getting cured? How will it fare in the wake to a sudden epidemic or a disaster? How are all of these affected by administrative decisions such as allocating/diminishing resources in various areas or centralising services? These are the questions motivating our study on a formal prototype model for a healthcare system. We propose that a healthcare system can be understood as a distributed system with independent nodes (healthcare providers) computing according to their own resources and constraints, with tasks (patient needs) being allocated between the nodes. The questions about the healthcare system become in this context questions about resource availability and distribution between the nodes. We construct in this paper an Event-B model capturing the basic functionality of a simplified healthcare system: patients with different types of medical needs being allocated to suitable medical providers, and navigating between different providers for their turn for multi-step treatments.

Słowa kluczowe

EN

medical personnel; medical care; prototype; curing

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 171, nr 1-4
• Strony: 331--343
• Opis fizyczny: Bibliogr. 20 poz. rys., tab.

Twórcy

autor

Petre Luigia

• Distributed Systems Laboratory, Åbo Akademi University and Turku Centre for Computer Science, Finland

autor

Sanwal Usman

• Computational Biomodeling Laboratory, Åbo Akademi University and Turku Centre for Computer Science, Finland

autor

Shah Gohar

• Computational Biomodeling Laboratory, Åbo Akademi University and Turku Centre for Computer Science, Finland

autor

Panchal Charmi

• Computational Biomodeling Laboratory, Åbo Akademi University and Turku Centre for Computer Science, Finland

autor

Tyagi Dwitiya

• Computational Biomodeling Laboratory, Åbo Akademi University and Turku Centre for Computer Science, Finland

autor

Petre Ion

• Computational Biomodeling Laboratory, University of Turku and Turku Centre for Computer Science, Finland
• National Institute for Research and Development in Biological Sciences, Romania

Bibliografia

• [1] Abrial JR. Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY, USA, 1st edition, 2010. ISBN 0521895561, 9780521895569.
• [2] Abrial JR. The B-book: Assigning Programs to Meanings. Cambridge University Press, New York, NY, USA, 1996. ISBN 0-521-49619-5.
• [3] Back RJ, Kurki-Suonio R. Decentralization of Process Nets with Centralized Control. In: Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, PODC ’83. ACM, New York, NY, USA. ISBN 0-89791-110-5, 1983 pp. 131-142. doi:10.1145/800221.806716. URL http: //doi.acm.org/10.1145/800221.806716.
• [4] Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Soft- ware Engineers. Addison-Wesley, 2003.
• [5] Chandy KM, Misra J. Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1988. ISBN 0-201-05866-9.
• [6] Butler M, Yadav D. An incremental development of the Mondex system in Event-B. Formal Aspects of Computing, 2007. 20(1):61-77. doi:10.1007/s00165-007-0061-4. URL http://dx.doi.org/10.1007/s00165-007-0061-4.
• [7] Lanoix A. Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles. In: Theoretical Aspects of Software Engineering. IEEE Computer Society, Los Alamitos, CA, USA. ISBN 978-0-7695-3249-3, 2008 pp. 297-304. doi:http://doi.ieeecomputersociety.org/10.1109/TASE.2008.39.
• [8] Hoang TS, Kuruma H, Basin D, Abrial JR. Developing Topology Discovery in Event-B. In: Leuschel M, Wehrheim H (eds.), Integrated Formal Methods, volume LNCS 5423. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-00255-7, 2009 pp. 1-19. doi:10.1007/978-3-642-00255-7_1. URL http://dx.doi.org/10.1007/978-3-642-00255-7_1.
• [9] Kamali M, Laibinis L, Petre L, Sere K. Self-Recovering Sensor-Actor Networks. In: Proceedings Ninth International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA 2010, Paris, France, 4th September 2010. 2010 pp. 47-61. doi:10.4204/EPTCS.30.4. URL http://dx.doi.org/10.4204/EPTCS.30.4.
• [10] Salehi Fathabadi A, Rezazadeh A, Butler M. Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. In: Bobaru M, Havelund K, Holzmann GJ, Joshi R (eds.), NASA Formal Methods. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-20398-5, 2011 pp. 328-342. doi:10.1007/978-3-642-20398-5_24. URL http://dx.doi.org/10.1007/978-3-642-20398-5_24.
• [11] Petre L, Sandvik P, Sere K. Node Coordination in Peer-to-Peer Networks. In: Coordination Models and Languages - 14th International Conference, COORDINATION 2012, Stockholm, Sweden, June 14-15, 2012. Proceedings. 2012 pp. 196-211. doi:10.1007/978-3-642-30829-1_14. URL http://dx.doi.org/10.1007/978-3-642-30829-1_14.
• [12] Horsmanheimo S, Kamali M, Kolehmainen M, Neovius M, Petre L, Rönkkö M, Sandvik P. On Proving Recoverability of Smart Electrical Grids. In: NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings. 2014 pp. 77-91. doi:10.1007/978-3-319-06200-6_6. URL http://dx.doi.org/10.1007/978-3-319-06200-6_6.
• [13] Kamali M, Höfner P, Kamali M, Petre L. Formal Analysis of Proactive, Distributed Routing. In: Software Engineering and Formal Methods - 13th International Conference, SEFM 2015, York, UK, September 7-11, 2015. Proceedings. 2015 pp. 175-189. doi:10.1007/978-3-319-22969-0_13. URL http://dx.doi.org/10.1007/978-3-319-22969-0_13.
• [14] Abrial JR, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L. Rodin: an open toolset for modelling and reasoning in Event-B. STTT, 2010. 12(6):447-466.
• [15] Maamria I, Butler M, Edmunds A, Rezazadeh A. On an Extensible Rule-Based Prover for Event-B. In: Frappier M, Glässer U, Khurshid S, Laleau R, Reeves S (eds.), Abstract State Machines, Alloy, B and Z, volume LNCS 5977. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-11811-1, 2010 pp. 407-407. doi:10.1007/978-3-642-11811-1_40. URL http://dx.doi.org/10.1007/978-3-642-11811-1_40.
• [16] Baksi D. Formal interaction specification in public health surveillance systems using pi-calculus. Comput Methods Programs Biomed, 2008. 92(1):115-120. doi:10.1016/j.cmpb.2008.05.007.
• [17] ten Teije A, Marcos M, Balser M, van Croonenborg J, Duelli C, van Harmelen F, Lucas P, Miksch S, Reif W, Rosenbrand K, Seyfang A. Improving medical protocols by formal methods. Artif Intell Med, 2006. 36(3):193-209. doi:10.1016/j.artmed.2005.10.006.
• [18] Bottrighi A, Giordano L, Molino G, Montani S, Terenziani P, Torchio M. Adopting model checking techniques for clinical guidelines verification. Artif Intell Med, 2010. 48(1):1-19. doi:10.1016/j.artmed.2009.09.003.
• [19] Christov S, Chen B, Avrunin GS, Clarke LA, Osterweil LJ, Brown D, Cassells L, Mertens W. Formally defining medical processes. Methods Inf Med, 2008. 47(5):392-398.
• [20] Bowles J, Caminati MB, Cha S. An integrated framework for verifying multiple care pathways. In: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE). 2017 pp. 1-8. doi:10.1109/TASE.2017.8285628.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).