Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A Secure User-Centred Healthcare System: Design and Verification

  • Conference paper
  • First Online:
From Data to Models and Back (DataMod 2021)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13268))

Included in the following conference series:

Abstract

With ever increasing amounts of travel, it is essential to have access to a patient’s medical data from different sources including many jurisdictions. The Serums project addresses this goal by creating a healthcare sharing system that places privacy and security aspects at the center. This raises significant challenges to both maintain privacy and security of medical data and to allow for sharing and access. To address these strict requirements the Serums system design is supported by formal methods where design decisions are modelled and checked to meet safety and security properties. We report an experience in support of the system design with formal modelling with the Uppaal tool and analysis with exhaustive and statistical model checking. Results show that statistical model checking being a simulation-based technique can significantly improve feasibility of analysis while providing support for design decisions to ensure privacy and security.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 59.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Information on GDPR can be found at https://gdpr-info.eu/.

  2. 2.

    For more information refer to https://www.serums-h2020.org.

  3. 3.

    It is possible to simplify the property by checking it separately for each doctor, however the simplification doesn’t affect RAM consumption while single doctor check takes almost the same time as the check for all doctors.

References

  1. Uppaal. https://www.uppaal.org

  2. Abdellatif, T., Brousmiche, K.L.: Formal verification of smart contracts based on users and blockchain behaviors models. In: 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1–5. IEEE (2018)

    Google Scholar 

  3. Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. (TOMACS) 28(1), 1–39 (2018)

    Article  MathSciNet  Google Scholar 

  4. Arnold, A.: Finite Transition Systems - Semantics of Communicating Systems. Prentice Hall International Series in Computer Science, Prentice Hall (1994)

    Google Scholar 

  5. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)

    Google Scholar 

  6. Baranov, E., Given-Wilson, T., Legay, A.: Improving Secure and Robust Patient Service Delivery. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 404–418. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-61362-4_23

    Chapter  Google Scholar 

  7. Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. Int. J. Softw. Tools Technol. Transfer 14(1), 53–72 (2012)

    Article  Google Scholar 

  8. ter Beek, M.H., et al.: Adopting formal methods in an industrial setting: the railways case. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 762–772. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_46

  9. Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Formal Methods for the Design of Real-Time Systems, pp. 200–236. Springer (2004). https://doi.org/10.1007/978-3-540-30080-9_7

  10. Bowles, J., Mendoza-Santana, J., Vermeulen, A.F., Webber, T., Blackledge, E.: Integrating healthcare data for enhanced citizen-centred care and analytics. Stud. Health Tech. Inf. 275, 17–21 (2020)

    Google Scholar 

  11. Bowles, J., Mendoza-Santana, J., Webber, T.: Interacting with next-generation smart patient-centric healthcare systems. In: UMAP’20 Adjunct: Adjunct Publication of the 28th ACM Conference on User Modeling, Adaptation and Personalization, pp. 192–193, July 2020

    Google Scholar 

  12. Bulychev, P., et al.: Monitor-based statistical model checking for weighted metric temporal logic. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 168–182. Springer (2012). https://doi.org/10.1007/978-3-642-28717-6_15

  13. Cerone, A., Elbegbayan, N.: Model-checking driven design of interactive systems. Electron. Notes Theor. Comput. Sci. 183, 3–20 (2007)

    Article  Google Scholar 

  14. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774

    Chapter  Google Scholar 

  15. Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1–30. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35746-6_1

    Chapter  Google Scholar 

  16. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transfer 17(4), 397–415 (2015)

    Google Scholar 

  17. David, A., et al.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24310-3

  18. Ellen, C., Gerwinn, S., Fränzle, M.: Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains. Int. J. Softw. Tools Technol. Transfer 17(4), 485–504 (2014). https://doi.org/10.1007/s10009-014-0329-y

    Article  Google Scholar 

  19. Gavrilov, G., Vlahu-Gjorgievska, E., Trajkovik, V.: Healthcare data warehouse system supporting cross-border interoperability. Health Informat. J. 26(2), 1321–1332 (2020)

    Article  Google Scholar 

  20. Gu, R., Enoiu, E., Seceleanu, C.: TAMAA: Uppaal-based mission planning for autonomous agents. In: Proceedings of the 35th Annual ACM Symposium on Applied Computing, pp. 1624–1633 (2020)

    Google Scholar 

  21. Harrison, M.D., Masci, P., Campos, J.C.: Formal modelling as a component of user centred design. In: Mazzara, M., Ober, I., Salaün, G. (eds.) STAF 2018. LNCS, vol. 11176, pp. 274–289. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-04771-9_21

    Chapter  Google Scholar 

  22. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24622-0_8

  23. Janjic, V., Bowles, J., Vermeulen, A., et al.: The serums tool-chain: ensuring security and privacy of medical data in smart patient-centric healthcare systems. In: 2019 IEEE International Conference on Big Data, pp. 2726–2735, December 2019

    Google Scholar 

  24. Jetley, R., Iyer, S.P., Jones, P.: A formal methods approach to medical device review. Computer 39(4), 61–67 (2006)

    Article  Google Scholar 

  25. Kalajdzic, K., et al.: Feedback control for statistical model checking of cyber-physical systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 46–61. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_4

  26. Kwiatkowska, M., Lea-Banks, H., Mereacre, A., Paoletti, N.: Formal modelling and validation of rate-adaptive pacemakers. In: 2014 IEEE International Conference on Healthcare Informatics, pp. 23–32. IEEE (2014)

    Google Scholar 

  27. Larrucea, X., Moffie, M., Asaf, S., Santamaria, I.: Towards a GDPR compliant way to secure European cross border healthcare industry 4.0. Comput. Stand. Interf. 69, 103408 (2020)

    Google Scholar 

  28. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: International Conference on Runtime Verification, pp. 122–135. Springer (2010). https://doi.org/10.1007/978-3-642-16612-9_11

  29. Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Computing and Software Science, pp. 478–504. Springer (2019). https://doi.org/10.1007/978-3-319-91908-9_23

  30. McGhin, T., Choo, K.K.R., Liu, C.Z., He, D.: Blockchain in healthcare applications: research challenges and opportunities. J. Netw. Comput. Appl. 135, 62–75 (2019)

    Article  Google Scholar 

  31. Mercaldo, F., Martinelli, F., Santone, A.: Real-time SCADA attack detection by means of formal methods. In: 2019 IEEE 28th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pp. 231–236. IEEE (2019)

    Google Scholar 

  32. Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: International Symposium on Programming. pp. 337–351. Springer (1982). https://doi.org/10.1007/3-540-11494-7_22

  33. Ravn, A.P., Srba, J., Vighio, S.: Modelling and verification of web services business activity protocol. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 357–371. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_32

    Chapter  Google Scholar 

  34. Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266–280. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_26

  35. Tanwar, S., Parekh, K., Evans, R.: Blockchain-based electronic healthcare record system for healthcare 4.0 applications. J. Inf. Secur. Appl. 50, 102407 (2020)

    Google Scholar 

  36. Ter Beek, M.H., Legay, A., Lafuente, A.L., Vandin, A.: A framework for quantitative modeling and analysis of highly (re) configurable systems. IEEE Trans. Software Eng. 46(3), 321–345 (2018)

    Article  Google Scholar 

  37. Webber, T., Santana, J.M., Vermeulen, A.F., Bowles, J.K.F.: Designing a patient-centric system for secure exchanges of medical data. In: Gervasi, O., et al. (eds.) ICCSA 2020. LNCS, vol. 12254, pp. 598–614. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58817-5_44

  38. Zuliani, P.: Statistical model checking for biological applications. Int. J. Softw. Tools Technol. Transfer 17(4), 527–536 (2014). https://doi.org/10.1007/s10009-014-0343-0

    Article  Google Scholar 

Download references

Acknowledgements

This research is funded by the EU H2020 project SERUMS (grant 826278). We thank Matthew Banton from the University of St Andrews for comments that greatly improved the platform security properties and Serums partners from Accenture and Sopra Steria for their help on the architectural diagrams design.

Author information

Authors and Affiliations

  1. Computer Science and Engineering Department, Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Eduard Baranov, Thomas Given-Wilson & Axel Legay

  2. School of Computer Science, University of St Andrews, St Andrews, KY16 9SX, UK

    Juliana Bowles & Thais Webber

Authors
  1. Eduard Baranov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Juliana Bowles
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thomas Given-Wilson
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Thais Webber
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Eduard Baranov .

Editor information

Editors and Affiliations

  1. University of St Andrews, St Andrews, UK

    Juliana Bowles

  2. ISTI-CNR, Pisa, Italy

    Giovanna Broccia

  3. University of Pisa, Pisa, Italy

    Roberto Pellungrini

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Baranov, E., Bowles, J., Given-Wilson, T., Legay, A., Webber, T. (2022). A Secure User-Centred Healthcare System: Design and Verification. In: Bowles, J., Broccia, G., Pellungrini, R. (eds) From Data to Models and Back. DataMod 2021. Lecture Notes in Computer Science, vol 13268. Springer, Cham. https://doi.org/10.1007/978-3-031-16011-0_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-16011-0_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-16010-3

  • Online ISBN: 978-3-031-16011-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation