{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T02:40:07Z","timestamp":1772160007460,"version":"3.50.1"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"19","license":[{"start":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T00:00:00Z","timestamp":1721779200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T00:00:00Z","timestamp":1721779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Soft Comput"],"published-print":{"date-parts":[[2024,10]]},"DOI":"10.1007\/s00500-024-09902-w","type":"journal-article","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T12:05:30Z","timestamp":1721822730000},"page":"10943-10963","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Service to service communication based on CBPS system: refinement and verification"],"prefix":"10.1007","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4318-4415","authenticated-orcid":false,"given":"Sarah Hussein","family":"Toman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aida","family":"Lahouij","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sonia","family":"Kotel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lazhar","family":"Hamel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zinah Hussein","family":"Toman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Graiet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,24]]},"reference":[{"key":"9902_CR1","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1109\/SCC.2011.42","volume-title":"2011 IEEE international conference on services computing","author":"L Abidi","year":"2011","unstructured":"Abidi L, C\u00e9rin C, Evangelista S (2011) A petri-net model for the publish\u2013subscribe paradigm and its application for the verification of the bonjourgrid middleware. 2011 IEEE international conference on services computing. IEEE, New York, pp 496\u2013503"},{"key":"9902_CR2","volume-title":"The B-book\u2014assigning programs to meanings","author":"J-R Abrial","year":"2005","unstructured":"Abrial J-R (2005) The B-book\u2014assigning programs to meanings. Cambridge University Press, Cambridge"},{"key":"9902_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: system and software engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge"},{"key":"9902_CR4","first-page":"1","volume-title":"Integrated formal methods: 10th international conference, IFM 2013, Turku, Finland, 10\u201314 June 2013, proceedings 10","author":"J-R Abrial","year":"2013","unstructured":"Abrial J-R (2013) From z to b and then Event-B: assigning proofs to meaningful programs. Integrated formal methods: 10th international conference, IFM 2013, Turku, Finland, 10\u201314 June 2013, proceedings 10. Springer, Berlin, pp 1\u201315"},{"key":"9902_CR5","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-91271-4_3","volume-title":"Abstract state machines, alloy, B, TLA, VDM, and Z: 6th international conference, ABZ 2018, Southampton, UK, 5\u20138 June 2018, proceedings 6","author":"J-R Abrial","year":"2018","unstructured":"Abrial J-R (2018) On B and Event-B: principles, success and challenges. Abstract state machines, alloy, B, TLA, VDM, and Z: 6th international conference, ABZ 2018, Southampton, UK, 5\u20138 June 2018, proceedings 6. Springer, Berlin, pp 31\u201335"},{"issue":"1\u20132","key":"9902_CR6","first-page":"1","volume":"77","author":"J-R Abrial","year":"2007","unstructured":"Abrial J-R, Hallerstede S (2007) Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fund Inform 77(1\u20132):1\u201328","journal-title":"Fund Inform"},{"key":"9902_CR7","doi-asserted-by":"crossref","unstructured":"Aguilera MK, Strom RE, Sturman DC, Astley M, Chandra TD (1999) Matching events in a content-based subscription system. In: Proceedings of the eighteenth annual ACM symposium on principles of distributed computing, pp 53\u201361","DOI":"10.1145\/301308.301326"},{"key":"9902_CR8","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.adhoc.2015.05.013","volume":"36","author":"B Aziz","year":"2016","unstructured":"Aziz B (2016) A formal model and analysis of an IOT protocol. Ad Hoc Netw 36:49\u201357","journal-title":"Ad Hoc Netw"},{"key":"9902_CR9","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/BF01214918","volume":"8","author":"RJR Back","year":"1996","unstructured":"Back RJR, Sere K (1996) Superposition refinement of reactive systems. Formal Aspects Comput 8:324\u2013346","journal-title":"Formal Aspects Comput"},{"key":"9902_CR10","doi-asserted-by":"crossref","unstructured":"Baldoni R, Beraldi R, Tucci Piergiovanni S, Virgillito A (2005) On the modelling of publish\/subscribe communication systems. Concurrency and Computation: Pract Exp 17(12):1471\u20131495","DOI":"10.1002\/cpe.879"},{"key":"9902_CR11","doi-asserted-by":"crossref","unstructured":"Banavar G, Chandra T, Mukherjee B, Nagarajarao J, Strom RE, Sturman DC (1999) An efficient multicast protocol for content-based publish\u2013subscribe systems. In: Proceedings. 19th IEEE international conference on distributed computing systems (cat. no. 99CB37003). IEEE, New York, pp 262\u2013272","DOI":"10.1109\/ICDCS.1999.776528"},{"key":"9902_CR12","doi-asserted-by":"crossref","unstructured":"Baresi L, Ghezzi C, Mottola L (2006a) Towards fine-grained automated verification of publish\u2013subscribe architectures. In: Formal techniques for networked and distributed systems\u2014FORTE 2006: 26th IFIP WG 6.1 international conference, Paris, France, 26\u201329 September 2006, proceedings 26. Springer, Berlin, pp 131\u2013135","DOI":"10.1007\/11888116_10"},{"key":"9902_CR13","doi-asserted-by":"crossref","unstructured":"Baresi L, Ghezzi C, Mottola L (2006b) Towards fine-grained automated verification of publish\u2013subscribe architectures. In: Formal techniques for networked and distributed systems\u2014FORTE 2006: 26th IFIP WG 6.1 international conference, Paris, France, 26\u201329 September 2006, proceedings 26. Springer, pp 131\u2013135","DOI":"10.1007\/11888116_10"},{"key":"9902_CR14","doi-asserted-by":"crossref","unstructured":"Baresi L, Gerosa G, Ghezzi C, Mottola L (2007a) Playing with time in publish\u2013subscribe using a domain-specific model checker. In: Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th joint meeting of the European conference on software engineering and the ACM SIGSOFT symposium on the foundations of software engineering, pp 55\u201362","DOI":"10.1145\/1292316.1292323"},{"key":"9902_CR15","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1109\/ICSE.2007.57","volume-title":"29th international conference on software engineering (ICSE\u201907)","author":"L Baresi","year":"2007","unstructured":"Baresi L, Ghezzi C, Mottola L (2007b) On accurate automatic verification of publish\u2013subscribe architectures. 29th international conference on software engineering (ICSE\u201907). IEEE, New York, pp 199\u2013208"},{"key":"9902_CR16","doi-asserted-by":"publisher","first-page":"929","DOI":"10.1109\/INFCOM.2004.1356980","volume-title":"IEEE INFOCOM 2004","author":"F Cao","year":"2004","unstructured":"Cao F, Singh JP (2004) Efficient event routing in content-based publish\u2013subscribe service networks. IEEE INFOCOM 2004, vol 2. IEEE, New York, pp 929\u2013940"},{"key":"9902_CR17","unstructured":"Corsaro A, Querzoni L, Scipioni S, Tucci Piergiovanni S, Virgillito A et al (2006) Quality of service in publish\/subscribe middleware. Global Data Management 19(20):1\u201322"},{"key":"9902_CR18","unstructured":"Delzanno G (2019) Towards the automated verification of publish\/subscribe networks. In Proceedings of the 1st workshop on artificial intelligence and formal verification, logics, automata and synthesis (OVERLAY), Rende, Italy, 19\u201320 November 2019, pp 35\u201340"},{"key":"9902_CR19","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s10009-019-00548-w","volume":"22","author":"D Dghaym","year":"2020","unstructured":"Dghaym D, Dalvandi M, Poppleton M, Snook C (2020) Formalising the hybrid ERTMS level 3 specification in iUML-b and Event-B. Int J Softw Tools Technol Transfer 22:297\u2013313","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"9902_CR20","doi-asserted-by":"crossref","unstructured":"D\u00edaz G, Cambronero ME, Maci\u00e1 H, Valero V (2015) Model-checking verification of publish\u2013subscribe architectures in web service contexts. In: Proceedings of the 30th annual ACM symposium on applied computing, pp 1688\u20131695","DOI":"10.1145\/2695664.2695744"},{"key":"9902_CR21","doi-asserted-by":"crossref","unstructured":"Diwan M, D\u2019Souza M (2017) A framework for modeling and verifying IOT communication protocols. In: Dependable software engineering. theories, tools, and applications: third international symposium, SETTA 2017, Changsha, China, 23\u201325 October 2017, proceedings 3. Springer, Berlin, pp 266\u2013280","DOI":"10.1007\/978-3-319-69483-2_16"},{"key":"9902_CR22","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-44829-2_11","volume-title":"Model checking software: 10th international SPIN workshop, Portland, OR, USA, 9\u201310 May 2003, proceedings 10","author":"D Garlan","year":"2003","unstructured":"Garlan D, Khersonsky S, Kim JS (2003) Model checking publish\u2013subscribe systems. Model checking software: 10th international SPIN workshop, Portland, OR, USA, 9\u201310 May 2003, proceedings 10. Springer, Berlin, pp 166\u2013180"},{"key":"9902_CR23","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-87603-8_11","volume-title":"Abstract state machines, B and Z: first international conference, ABZ 2008, London, UK, 16\u201318 September 2008, proceedings 1","author":"S Hallerstede","year":"2008","unstructured":"Hallerstede S (2008) On the purpose of Event-B proof obligations. Abstract state machines, B and Z: first international conference, ABZ 2008, London, UK, 16\u201318 September 2008, proceedings 1. Springer, Berlin, pp 125\u2013138"},{"key":"9902_CR24","doi-asserted-by":"crossref","unstructured":"He F, Baresi L, Ghezzi C, Spoletini P (2007) Formal analysis of publish\u2013subscribe systems by probabilistic timed automata. In: Formal techniques for networked and distributed systems\u2014FORTE 2007: 27th IFIP WG 6.1 international conference, Tallinn, Estonia, 27\u201329 June 2007, proceedings 27. Springer, Berlin, pp 247\u2013262","DOI":"10.1007\/978-3-540-73196-2_16"},{"key":"9902_CR25","first-page":"211","volume-title":"Industrial deployment of system engineering methods","author":"TS Hoang","year":"2013","unstructured":"Hoang TS (2013) An introduction to the Event-B modelling method. Industrial deployment of system engineering methods. Springer, Berlin, pp 211\u2013236"},{"key":"9902_CR26","doi-asserted-by":"crossref","unstructured":"Khelifi S, Kacem HH, Kacem AH (2008) Specification and verification of the structural and behavioral properties of publish\/subscribe architectures. In: Second international workshop on verification and evaluation of computer and communication systems (VECoS 2008), pp 1\u201310","DOI":"10.14236\/ewic\/VECOS2008.17"},{"issue":"4","key":"9902_CR27","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1016\/j.compind.2013.02.008","volume":"64","author":"Y Laili","year":"2013","unstructured":"Laili Y, Tao F, Zhang L, Cheng Y, Luo Y, Sarker BR (2013) A ranking chaos algorithm for dual scheduling of cloud service and computing resource in private cloud. Comput Ind 64(4):448\u2013463","journal-title":"Comput Ind"},{"key":"9902_CR28","doi-asserted-by":"publisher","DOI":"10.1016\/j.iot.2022.100538","volume":"19","author":"A Lazidis","year":"2022","unstructured":"Lazidis A, Tsakos K, Petrakis EGM (2022) Publish\u2013subscribe approaches for the IOT and the cloud: functional and performance evaluation of open-source systems. Internet of Things 19:100538","journal-title":"Internet of Things"},{"key":"9902_CR29","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: formal methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel M, Butler M (2003) Prob: a model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods. Springer, Berlin, pp 855\u2013874"},{"key":"9902_CR30","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/11587552_13","volume-title":"Middleware 2005: ACM\/IFIP\/USENIX 6th international middleware conference, Grenoble, France, 28 November\u20132 December 2005, proceedings 6","author":"G Li","year":"2005","unstructured":"Li G, Jacobsen H-A (2005) Composite subscriptions in content-based publish\/subscribe systems. Middleware 2005: ACM\/IFIP\/USENIX 6th international middleware conference, Grenoble, France, 28 November\u20132 December 2005, proceedings 6. Springer, Berlin, pp 249\u2013269"},{"key":"9902_CR31","unstructured":"Mladenov K, Van Winsen S, Mavrakis C, Cyber K (2017) Formal verification of the implementation of the MQTT protocol in IOT devices. In: SNE master research projects 2016\u20132017"},{"key":"9902_CR34","first-page":"1","volume-title":"2006 Securecomm and workshops","author":"C Raiciu","year":"2006","unstructured":"Raiciu C, Rosenblum DS (2006) Enabling confidentiality in content-based publish\/subscribe infrastructures. 2006 Securecomm and workshops. IEEE, New York, pp 1\u201311"},{"key":"9902_CR35","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.scico.2014.04.015","volume":"94","author":"W Su","year":"2014","unstructured":"Su W, Abrial J-R, Zhu H (2014) Formalizing hybrid systems with Event-B and the rodin platform. Sci Comput Program 94:164\u2013202","journal-title":"Sci Comput Program"},{"key":"9902_CR36","doi-asserted-by":"publisher","first-page":"2598","DOI":"10.1016\/j.procs.2022.09.318","volume":"207","author":"ZH Toman","year":"2022","unstructured":"Toman ZH, Hamel L, Toman SH, Graiet M (2022) Correct-by-construction approach for formal verification of IOT architecture. Procedia Comput Sci 207:2598\u20132609","journal-title":"Procedia Comput Sci"},{"key":"9902_CR37","doi-asserted-by":"crossref","unstructured":"Toman SH, Hamel L, Toman ZH, Graiet M, Ouchani S (2023a) Formal modelling and verification of scalable service composition in IOT environment. In: Service oriented computing and applications, pp 1\u201319","DOI":"10.1007\/s11761-023-00363-x"},{"key":"9902_CR38","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s40860-023-00202-y","volume":"10","author":"ZH Toman","year":"2023","unstructured":"Toman ZH, Hamel L, Toman SH, Graiet M, Valadares DCG (2023b) Formal verification for security and attacks in IOT physical layer. J Reliab Intell Environ 10:73\u201391","journal-title":"J Reliab Intell Environ"},{"key":"9902_CR39","doi-asserted-by":"crossref","unstructured":"Toman SH, Hamel L, Graiet M (2023c) Refinement and verification for IOT service composition. In: 2023 IEEE symposium on computers and communications (ISCC), pp 483\u2013486","DOI":"10.1109\/ISCC58397.2023.10218287"},{"issue":"4","key":"9902_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J (2009) Formal methods: practice and experience. ACM Comput Surv (CSUR) 41(4):1\u201336","journal-title":"ACM Comput Surv (CSUR)"},{"issue":"1","key":"9902_CR41","doi-asserted-by":"publisher","first-page":"277","DOI":"10.2298\/CSIS210707057X","volume":"20","author":"J Xu","year":"2023","unstructured":"Xu J, Yin J, Zhu H, Xiao L (2023) Formalization and verification of Kafka messaging mechanism using CSP. Comput Sci Inf Syst 20(1):277\u2013306","journal-title":"Comput Sci Inf Syst"},{"key":"9902_CR42","volume-title":"Efficient content-based publish\/subscribe systems for dynamic and large-scale networked applications","author":"Y Zhao","year":"2012","unstructured":"Zhao Y (2012) Efficient content-based publish\/subscribe systems for dynamic and large-scale networked applications. Temple University, Philadelphia"}],"container-title":["Soft Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-024-09902-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00500-024-09902-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-024-09902-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T07:08:00Z","timestamp":1729321680000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00500-024-09902-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,24]]},"references-count":40,"journal-issue":{"issue":"19","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["9902"],"URL":"https:\/\/doi.org\/10.1007\/s00500-024-09902-w","relation":{},"ISSN":["1432-7643","1433-7479"],"issn-type":[{"value":"1432-7643","type":"print"},{"value":"1433-7479","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,24]]},"assertion":[{"value":"7 May 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 July 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Informed consent was obtained from all individual participants included in the study.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Informed consent"}},{"value":"This article does not contain any studies with animals performed by any of the authors.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Research involving human participants and\/or animals"}}]}}