Formal Method in Service Composition in Heath Care Systems
Subject Areas : Software Architecture
Zahra Baatmaanghelich
1
(
Department of Computer Engineering, Science and Research Branch, Islamic Azad University, Tehran, Iran
)
Ali Rezaee
2
(
Department of Computer Engineering, Science and Research Branch, Islamic Azad University, Tehran, Iran
)
Sahar Adabi
3
(
Department of Computer Engineering, Tehran-North Branch, Islamic Azad University, Tehran, Iran
)
Keywords: Model checking, Formal methods, Pervasive healthcare, CSP, BPMN,
Abstract :
One of the areas with greatest needs having available information at the right moment and with high accuracy is healthcare. Right information at right time saves lives. Healthcare is a vital domain which needs high processing power for high amounts of data. Due to the critical and the special characteristics of these systems, formal methods are used for specification, description and verification. The goal of this research is to turn a business process graphical diagram into a formal based model. In this work, BPMN has been extended to add time and probability information and then has been transferred to probabilistic real-time CSP area. This mapping can be employed as a basic model for modeling different system characteristics. This mapping, then, is modeled using a case study in pervasive healthcare domain and verified in a model checking tool. Index Terms — Formal methods, CSP, BPMN, Pervasive healthcare, Model checking, Verification, Service Composition.
[1] Quan Z. Sheng, Xiaoqiang Qiao, Athanasios V. Vasilakos, Claudia Szabo, Scott Bourne, Xiaofei Xu, 2014, “Web services Composition: A decade’s overview”, Elsevier, Information Sciences.
[2] Oana-Sorina Lupşe, Mihaela Marcella Vida, Lăcrămioara Stoicu-Tivadar, 2012 , “Cloud Computing and Interoperability in Healthcare Information Systems”, INTELLI: The First International Conference on Intelligent Systems and Applications.
[3] Upkar Varshney, 2005, “Pervasive Heaithcare: Applicattions, Challenges and Wireless Solutions”, Communications of the Association for Information Systems, Volume 16, 57-72.
[4] Stephen A. White, 2016, “Process Modeling Notations and Workflow Patterns”, IBM Corp..
[5] Jakob Freund, Bernd Rücker, 2014, “Real-Life BPMN: Using BPMN 2.0 to Analyze, Improve, and Automate Processes in Your Company”.
[6] Stephen A. White, 2016, “BPMN Modeling and Reference Guide: Understanding and Using BPMN”, Future Strategies Inc.
[7] Andreas Lanz, Manfred Reichert, Barbara Weber, 2015, “Process time patterns: A formal foundation”, Elsevier, Information Systems.
[8] Saoussen Cheikhrouhou, Slim Kallel, Nawal Guermouche, Mohamed Jmaiel, 2015, “The Temporal Perspective in Business Process Modeling: An Evaluative Survey and Research Challenges”, Service Oriented Computing and Applications, Springer London, pp. 75-85.
[9] Outman El hichami, Mohammed Al achhab, Badr Eddine El Mohajir, , 2014, "Towards Formal Verification of Business Process using a Graphical Specification", IEEE.
[10] Guisheng Fan, Huiqun Yu, Liqiong Chen, Dongmei Liu, 2014, “Formal Modeling and Analyzing the Reliability for Service Composition”, IEEE.
[11] Ali Rezaee, Amir Masoud Rahmani, Ali Movaghar, Mohammad Teshnehlab, 2014, “Formal process algebraic modeling, verification, and analysis of an abstract Fuzzy Inference Cloud Service”, Springer Science, J Supercomput 67:345–383.
[12] Matthew Rodano, Kristin Giammarco, 2013, “A Formal Method for Evaluation of a Modeled System Architecture”, Computer Science 20, 210–215, Conference Organized by Missouri University of Science and Technology.
[13] W. Ait-Cheik-Bihi, A. Nait-Sidi-Moh, M. Bakhouya, J. Gaber, M. Wack, 2012, “Performance Study of Workflow Patterns-Based Web Service Composition”, Elsevier.
[14] C. Dumez, M. Bakhouya, J. Gaber, M. Wack, P. Lorenz, 2013, “Model-driven approach supporting formal verification for web service composition protocols”, Elsevier Ltd, Journal of Network and Computer Applications 36, 1102–1115.
[15] A.W. Roscoe, 2005, “The Theory and Practice of Concurrency”.
[16] Hoare CAR, 2004, “Communicating sequential processes”, Prentice Hall, Englewood Cliffs.