{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T04:53:24Z","timestamp":1749099204570,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031160103"},{"type":"electronic","value":"9783031160110"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-16011-0_4","type":"book-chapter","created":{"date-parts":[[2022,10,14]],"date-time":"2022-10-14T07:03:42Z","timestamp":1665731022000},"page":"44-60","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Secure User-Centred Healthcare System: Design and\u00a0Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7357-705X","authenticated-orcid":false,"given":"Eduard","family":"Baranov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5918-9114","authenticated-orcid":false,"given":"Juliana","family":"Bowles","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8700-2671","authenticated-orcid":false,"given":"Thomas","family":"Given-Wilson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2287-8925","authenticated-orcid":false,"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8091-6021","authenticated-orcid":false,"given":"Thais","family":"Webber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,15]]},"reference":[{"key":"4_CR1","unstructured":"Uppaal. https:\/\/www.uppaal.org"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"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\u20135. IEEE (2018)","DOI":"10.1109\/NTMS.2018.8328737"},{"issue":"1","key":"4_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. (TOMACS) 28(1), 1\u201339 (2018)","journal-title":"ACM Trans. Model. Comput. Simul. (TOMACS)"},{"key":"4_CR4","unstructured":"Arnold, A.: Finite Transition Systems - Semantics of Communicating Systems. Prentice Hall International Series in Computer Science, Prentice Hall (1994)"},{"key":"4_CR5","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-030-61362-4_23","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"E Baranov","year":"2020","unstructured":"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\u2013418. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_23"},{"issue":"1","key":"4_CR7","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10009-011-0201-2","volume":"14","author":"A Basu","year":"2012","unstructured":"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\u201372 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"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\u2013772. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_46","DOI":"10.1007\/978-3-030-30942-8_46"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Formal Methods for the Design of Real-Time Systems, pp. 200\u2013236. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"4_CR10","first-page":"17","volume":"275","author":"J Bowles","year":"2020","unstructured":"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\u201321 (2020)","journal-title":"Stud. Health Tech. Inf."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Bowles, J., Mendoza-Santana, J., Webber, T.: Interacting with next-generation smart patient-centric healthcare systems. In: UMAP\u201920 Adjunct: Adjunct Publication of the 28th ACM Conference on User Modeling, Adaptation and Personalization, pp. 192\u2013193, July 2020","DOI":"10.1145\/3386392.3399561"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"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\u2013182. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_15","DOI":"10.1007\/978-3-642-28717-6_15"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.01.058","volume":"183","author":"A Cerone","year":"2007","unstructured":"Cerone, A., Elbegbayan, N.: Model-checking driven design of interactive systems. Electron. Notes Theor. Comput. Sci. 183, 3\u201320 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"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\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1\u201330. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_1"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transfer 17(4), 397\u2013415 (2015)","DOI":"10.1007\/s10009-014-0361-y"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"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\u201396. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24310-3","DOI":"10.1007\/978-3-642-24310-3"},{"issue":"4","key":"4_CR18","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10009-014-0329-y","volume":"17","author":"C Ellen","year":"2014","unstructured":"Ellen, C., Gerwinn, S., Fr\u00e4nzle, M.: Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains. Int. J. Softw. Tools Technol. Transfer 17(4), 485\u2013504 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0329-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"1321","DOI":"10.1177\/1460458219876793","volume":"26","author":"G Gavrilov","year":"2020","unstructured":"Gavrilov, G., Vlahu-Gjorgievska, E., Trajkovik, V.: Healthcare data warehouse system supporting cross-border interoperability. Health Informat. J. 26(2), 1321\u20131332 (2020)","journal-title":"Health Informat. J."},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"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\u20131633 (2020)","DOI":"10.1145\/3341105.3374001"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-030-04771-9_21","volume-title":"Software Technologies: Applications and Foundations","author":"MD Harrison","year":"2018","unstructured":"Harrison, M.D., Masci, P., Campos, J.C.: Formal modelling as a component of user centred design. In: Mazzara, M., Ober, I., Sala\u00fcn, G. (eds.) STAF 2018. LNCS, vol. 11176, pp. 274\u2013289. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-04771-9_21"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_8","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"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\u20132735, December 2019","DOI":"10.1109\/BigData47090.2019.9005600"},{"issue":"4","key":"4_CR24","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/MC.2006.113","volume":"39","author":"R Jetley","year":"2006","unstructured":"Jetley, R., Iyer, S.P., Jones, P.: A formal methods approach to medical device review. Computer 39(4), 61\u201367 (2006)","journal-title":"Computer"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"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\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_4","DOI":"10.1007\/978-3-319-47166-2_4"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"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\u201332. IEEE (2014)","DOI":"10.1109\/ICHI.2014.11"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1016\/j.csi.2019.103408"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: International Conference on Runtime Verification, pp. 122\u2013135. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_11","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Computing and Software Science, pp. 478\u2013504. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_23","DOI":"10.1007\/978-3-319-91908-9_23"},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1016\/j.jnca.2019.02.027","volume":"135","author":"T McGhin","year":"2019","unstructured":"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\u201375 (2019)","journal-title":"J. Netw. Comput. Appl."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"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\u2013236. IEEE (2019)","DOI":"10.1109\/WETICE.2019.00057"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: International Symposium on Programming. pp. 337\u2013351. Springer (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22","DOI":"10.1007\/3-540-11494-7_22"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-19835-9_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AP Ravn","year":"2011","unstructured":"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\u2013371. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_32"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"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\u2013280. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_26","DOI":"10.1007\/11513988_26"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Tanwar, S., Parekh, K., Evans, R.: Blockchain-based electronic healthcare record system for healthcare 4.0 applications. J. Inf. Secur. Appl. 50, 102407 (2020)","DOI":"10.1016\/j.jisa.2019.102407"},{"issue":"3","key":"4_CR36","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1109\/TSE.2018.2853726","volume":"46","author":"MH Ter Beek","year":"2018","unstructured":"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\u2013345 (2018)","journal-title":"IEEE Trans. Software Eng."},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"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\u2013614. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58817-5_44","DOI":"10.1007\/978-3-030-58817-5_44"},{"issue":"4","key":"4_CR38","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/s10009-014-0343-0","volume":"17","author":"P Zuliani","year":"2014","unstructured":"Zuliani, P.: Statistical model checking for biological applications. Int. J. Softw. Tools Technol. Transfer 17(4), 527\u2013536 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0343-0","journal-title":"Int. J. Softw. Tools Technol. Transfer"}],"container-title":["Lecture Notes in Computer Science","From Data to Models and Back"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-16011-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,14]],"date-time":"2022-10-14T07:03:59Z","timestamp":1665731039000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-16011-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031160103","9783031160110"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-16011-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"15 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"DataMod","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium: From Data to Models and Back","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 December 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"datamod2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}