{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T21:15:04Z","timestamp":1757625304427,"version":"3.44.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2025,7,31]],"date-time":"2025-07-31T00:00:00Z","timestamp":1753920000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,7,31]],"date-time":"2025-07-31T00:00:00Z","timestamp":1753920000000},"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":["Cluster Comput"],"published-print":{"date-parts":[[2025,9]]},"DOI":"10.1007\/s10586-025-05127-0","type":"journal-article","created":{"date-parts":[[2025,7,31]],"date-time":"2025-07-31T12:45:38Z","timestamp":1753965938000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal service conflict detection through abstraction and refinement"],"prefix":"10.1007","volume":"28","author":[{"given":"Sarah Hussein","family":"Toman","sequence":"first","affiliation":[]},{"given":"Zinah Hussein","family":"Toman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,31]]},"reference":[{"issue":"1","key":"5127_CR1","doi-asserted-by":"publisher","first-page":"24","DOI":"10.3390\/systems5010024","volume":"5","author":"PJ Ryan","year":"2017","unstructured":"Ryan, P.J., Watson, R.B.: Research challenges for the internet of things: what role can or play? Systems 5(1), 24 (2017)","journal-title":"Systems"},{"issue":"4","key":"5127_CR2","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1177\/002234338402100403","volume":"21","author":"R V\u00e4yrynen","year":"1984","unstructured":"V\u00e4yrynen, R.: Regional conflict formations: an intractable problem of international relations. J. Peace Res. 21(4), 337\u2013359 (1984)","journal-title":"J. Peace Res."},{"issue":"3","key":"5127_CR3","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s11761-023-00363-x","volume":"17","author":"SH Toman","year":"2023","unstructured":"Toman, S.H., Hamel, L., Toman, Z.H., Graiet, M., Ouchani, S.: Formal modelling and verification of scalable service composition in IoT environment. SOCA 17(3), 213\u2013231 (2023)","journal-title":"SOCA"},{"issue":"1","key":"5127_CR4","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3390\/iot3010012","volume":"3","author":"P Pradeep","year":"2022","unstructured":"Pradeep, P., Kant, K.: Conflict detection and resolution in IoT systems: a survey. IoT 3(1), 191\u2013218 (2022)","journal-title":"IoT"},{"key":"5127_CR5","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: On b and Event-B: principles, success and challenges. In: Abstract State Machines, Alloy, B, TLA, VDM, and Z: 6th International Conference, ABZ 2018, Southampton, UK, June 5\u20138, 2018, Proceedings 6, pp. 31\u201335. Springer (2018)","DOI":"10.1007\/978-3-319-91271-4_3"},{"key":"5127_CR6","doi-asserted-by":"crossref","unstructured":"Toman, S.H., Hamel, L., Graiet, M.: Refinement and verification for IoT service composition. In: 2023 IEEE Symposium on Computers and Communications (ISCC), pp. 483\u2013486 (2023). https:\/\/doi.org\/10.1109\/ISCC58397.2023.10218287","DOI":"10.1109\/ISCC58397.2023.10218287"},{"key":"5127_CR7","first-page":"1","volume":"2021","author":"ZH Toman","year":"2023","unstructured":"Toman, Z.H., Hamel, L., Toman, S.H., Graiet, M., Valadares, D.C.G.: Formal verification for security and attacks in IoT physical layer. J. Reliab. Intell. Environ. 2021, 1\u201319 (2023)","journal-title":"J. Reliab. Intell. Environ."},{"key":"5127_CR8","doi-asserted-by":"crossref","unstructured":"Toman, S.H., Lahouij, A., Hamel, L., Toman, Z.H., Graiet, M.: A correct by construction model for cbps systems verification. In: 2023 IEEE Symposium on Computers and Communications (ISCC). pp. 1299\u20131304 (2023). https:\/\/doi.org\/10.1109\/ISCC58397.2023.10217842","DOI":"10.1109\/ISCC58397.2023.10217842"},{"key":"5127_CR9","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: From z to b and then Event-B: assigning proofs to meaningful programs. In: Integrated Formal Methods: 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013, Proceedings 10, pp. 1\u201315. Springer (2013)","DOI":"10.1007\/978-3-642-38613-8_1"},{"issue":"4","key":"5127_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. (CSUR) 41(4), 1\u201336 (2009)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"5127_CR11","first-page":"1","volume":"2024","author":"SH Toman","year":"2024","unstructured":"Toman, S.H., Lahouij, A., Kotel, S., Hamel, L., Toman, Z.H., Graiet, M.: Service to service communication based on CBPS system: refinement and verification. Soft. Comput. 2024, 1\u201321 (2024)","journal-title":"Soft. Comput."},{"key":"5127_CR12","doi-asserted-by":"crossref","unstructured":"Pradeep, P., Pal, A., Kant, K.: Automating conflict detection and mitigation in large-scale iot systems. In: 2021 IEEE\/ACM 21st International Symposium on Cluster, Cloud and Internet Computing (CCGrid), pp. 535\u2013544. IEEE (2021)","DOI":"10.1109\/CCGrid51090.2021.00063"},{"key":"5127_CR13","unstructured":"Al-Farooq, A., Al-Shaer, E., Kant, K.: A formal method for detecting rule conflicts in large scale IoT systems. In: IFIP\/IEEE IM (2019)"},{"issue":"10","key":"5127_CR14","doi-asserted-by":"publisher","first-page":"2607","DOI":"10.1109\/TIFS.2019.2899758","volume":"14","author":"KH Hsu","year":"2019","unstructured":"Hsu, K.H., Chiang, Y.H., Hsiao, H.C.: Safechain: securing trigger-action programming from attack chains. IEEE Trans. Inf. Forensics Secur. 14(10), 2607\u20132622 (2019)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"5127_CR15","doi-asserted-by":"crossref","unstructured":"Liu, R., Wang, Z., Garcia, L., Srivastava, M.: Remediot: Remedial actions for internet-of-things conflicts. In: Proceedings of the 6th ACM International Conference on Systems for Energy-Efficient Buildings, Cities, and Transportation, pp. 101\u2013110 (2019)","DOI":"10.1145\/3360322.3360837"},{"key":"5127_CR16","doi-asserted-by":"crossref","unstructured":"Celik, Z.B., Tan, G., McDaniel, P.D.: Iotguard: dynamic enforcement of security and safety policy in commodity IoT. In: NDSS (2019)","DOI":"10.14722\/ndss.2019.23326"},{"key":"5127_CR17","doi-asserted-by":"crossref","unstructured":"Ma, M., Preum, S.M., Stankovic, J.A.: Cityguard: a watchdog for safety-aware conflict detection in smart cities. In: Proceedings of the Second International Conference on Internet-of-Things Design and Implementation, pp. 259\u2013270 (2017)","DOI":"10.1145\/3054977.3054989"},{"key":"5127_CR18","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.pmcj.2013.06.001","volume":"12","author":"P Carreira","year":"2014","unstructured":"Carreira, P., Resendes, S., Santos, A.C.: Towards automatic conflict detection in home and building automation systems. Pervasive Mob. Comput. 12, 37\u201357 (2014)","journal-title":"Pervasive Mob. Comput."},{"issue":"2\u20133","key":"5127_CR19","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2006.11.002","volume":"67","author":"M Shehata","year":"2007","unstructured":"Shehata, M., Eberlein, A., Fapojuwo, A.: Using semi-formal methods for detecting interactions among smart homes policies. Sci. Comput. Program. 67(2\u20133), 125\u2013161 (2007)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"5127_CR20","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1016\/j.comnet.2006.08.011","volume":"51","author":"M Shehata","year":"2007","unstructured":"Shehata, M., Eberlein, A., Fapojuwo, A.O.: A taxonomy for identifying requirement interactions in software systems. Comput. Netw. 51(2), 398\u2013425 (2007)","journal-title":"Comput. Netw."},{"key":"5127_CR21","doi-asserted-by":"crossref","unstructured":"Newcomb, J.L., Chandra, S., Jeannin, J.B., Schlesinger, C., Sridharan, M.: Iota: a calculus for internet of things automation. In: Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, pp. 119\u2013133 (2017)","DOI":"10.1145\/3133850.3133860"},{"key":"5127_CR22","doi-asserted-by":"crossref","unstructured":"Bak, N., Chang, B.M., Choi, K.: Smart block: A visual programming environment for smart things. In: 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC), vol.\u00a02, pp. 32\u201337. IEEE (2018)","DOI":"10.1109\/COMPSAC.2018.10199"},{"key":"5127_CR23","doi-asserted-by":"crossref","unstructured":"Sen, J.: Internet of things: technology, applications and standardization. BoD\u2013Books on Demand (2018)","DOI":"10.5772\/intechopen.70907"},{"key":"5127_CR24","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s11036-018-1142-8","volume":"24","author":"W Xie","year":"2019","unstructured":"Xie, W., Zhu, H., Wu, X., Vinh, P.C.: Formal verification of mcwq using extended hoare logic. Mobile Netw. Appl. 24, 134\u2013144 (2019)","journal-title":"Mobile Netw. Appl."},{"issue":"4","key":"5127_CR25","doi-asserted-by":"publisher","first-page":"1255","DOI":"10.1007\/s11036-022-02046-x","volume":"28","author":"A Mu\u00f1oz","year":"2023","unstructured":"Mu\u00f1oz, A., Fern\u00e1ndez-Gago, C., L\u00f3pez-Villa, R.: A test environment for wireless hacking in domestic IoT scenarios. Mobile Netw. Appl. 28(4), 1255\u20131264 (2023)","journal-title":"Mobile Netw. Appl."},{"key":"5127_CR26","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, A., Ma\u00f1a, A., Gonz\u00e1lez, J.: Dynamic security properties monitoring architecture for cloud computing. In: Security Engineering for Cloud Computing: Approaches and Tools, pp. 1\u201318. IGI Global (2013)","DOI":"10.4018\/978-1-4666-2125-1.ch001"},{"key":"5127_CR27","doi-asserted-by":"crossref","unstructured":"Munoz, A., Mafia, A.: Software and hardware certification techniques in a combined certification model. In: 2014 11th International Conference on Security and Cryptography (SECRYPT), pp.\u00a01\u20136. IEEE (2014)","DOI":"10.5220\/0005098204050410"},{"key":"5127_CR28","volume-title":"Requirements Engineering in the Solution Domain","author":"E Hull","year":"2005","unstructured":"Hull, E., Jackson, K., Dick, J.: Requirements Engineering in the Solution Domain. Springer, Cham (2005)"},{"issue":"4","key":"5127_CR29","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2983528","volume":"60","author":"A Bouguettaya","year":"2017","unstructured":"Bouguettaya, A., Singh, M., Huhns, M., Sheng, Q.Z., Dong, H., Yu, Q., Neiat, A.G., Mistry, S., Benatallah, B., Medjahed, B., et al.: A service computing manifesto: the next 10 years. Commun. ACM 60(4), 64\u201372 (2017)","journal-title":"Commun. ACM"},{"key":"5127_CR30","doi-asserted-by":"crossref","unstructured":"Liang, C.J.M., Bu, L., Li, Z., Zhang, J., Han, S., Karlsson, B.F., Zhang, D., Zhao, F.: Systematically debugging iot control system correctness for building automation. In: Proceedings of the 3rd ACM International Conference on Systems for Energy-Efficient Built Environments, pp. 133\u2013142 (2016)","DOI":"10.1145\/2993422.2993426"},{"issue":"2","key":"5127_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3057861","volume":"24","author":"G Ghiani","year":"2017","unstructured":"Ghiani, G., Manca, M., Patern\u00f2, F., Santoro, C.: Personalization of context-dependent applications through trigger-action rules. ACM Trans. Comput. Human Interact. 24(2), 1\u201333 (2017)","journal-title":"ACM Trans. Comput. Human Interact."},{"key":"5127_CR32","doi-asserted-by":"crossref","unstructured":"Huang, B., Dong, H., Bouguettaya, A.: Conflict detection in IoT-based smart homes. In: 2021 IEEE International Conference on Web Services (ICWS), pp. 303\u2013313. IEEE (2021)","DOI":"10.1109\/ICWS53863.2021.00048"},{"key":"5127_CR33","doi-asserted-by":"crossref","unstructured":"Corradini, F., Culmone, R., Mostarda, L., Tesei, L., Raimondi, F.: A constrained ECA language supporting formal verification of WSNS. In: 2015 IEEE 29th International Conference on Advanced Information Networking and Applications Workshops, pp. 187\u2013192. IEEE (2015)","DOI":"10.1109\/WAINA.2015.109"},{"issue":"2","key":"5127_CR34","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/THMS.2014.2364613","volume":"45","author":"Y Sun","year":"2014","unstructured":"Sun, Y., Wang, X., Luo, H., Li, X.: Conflict detection scheme based on formal rule model for smart building systems. IEEE Trans. Human Mach. Syst. 45(2), 215\u2013227 (2014)","journal-title":"IEEE Trans. Human Mach. Syst."},{"key":"5127_CR35","doi-asserted-by":"publisher","DOI":"10.1016\/j.buildenv.2020.106983","volume":"181","author":"H Ibrhim","year":"2020","unstructured":"Ibrhim, H., Khattab, S., Elsayed, K., Badr, A., Nabil, E.: A formal methods-based rule verification framework for end-user programming in campus building automation systems. Build. Environ. 181, 106983 (2020)","journal-title":"Build. Environ."},{"key":"5127_CR36","doi-asserted-by":"publisher","first-page":"85072","DOI":"10.1109\/ACCESS.2024.3415632","volume":"12","author":"AM Ansari","year":"2024","unstructured":"Ansari, A.M., Nazir, M., Mustafa, K.: Ontology-based classification and detection of the smart home automation rules conflicts. IEEE Access 12, 85072\u201385088 (2024)","journal-title":"IEEE Access"},{"key":"5127_CR37","doi-asserted-by":"publisher","DOI":"10.1111\/exsy.13597","volume":"2024","author":"SS Kumar","year":"2024","unstructured":"Kumar, S.S., Agarwal, S.: Rule based complex event processing for IoT applications: review, classification and challenges. Expert. Syst. 2024, e13597 (2024)","journal-title":"Expert. Syst."},{"key":"5127_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1155\/2024\/4456261","volume":"2024","author":"R Yang","year":"2024","unstructured":"Yang, R., Wu, M., Gui, X., Chen, H.: Intelligent conflict detection of IoT services using high-level petri nets. Complex Intell. Syst. 2024, 1\u201329 (2024)","journal-title":"Complex Intell. Syst."},{"key":"5127_CR39","first-page":"211","volume-title":"Industrial Deployment of System Engineering Methods","author":"TS Hoang","year":"2013","unstructured":"Hoang, T.S.: An introduction to the Event-B modelling method. In: Industrial Deployment of System Engineering Methods, pp. 211\u2013236. Springer, Berlin (2013)"},{"key":"5127_CR40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"5127_CR41","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.: Formalising the hybrid ERTMS level 3 specification in iuml-b and Event-B. Int. J. Softw. Tools Technol. Transfer 22, 297\u2013313 (2020)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"5127_CR42","doi-asserted-by":"crossref","unstructured":"Hallerstede, S.: On the purpose of Event-B proof obligations. In: Abstract State Machines, B and Z: First International Conference, ABZ 2008, London, UK, September 16-18, 2008, Proceedings 1, pp. 125\u2013138. Springer (2008)","DOI":"10.1007\/978-3-540-87603-8_11"},{"key":"5127_CR43","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/BF01214918","volume":"8","author":"RJ Back","year":"1996","unstructured":"Back, R.J., Sere, K.: Superposition refinement of reactive systems. Formal Aspects Comput. 8, 324\u2013346 (1996)","journal-title":"Formal Aspects Comput."},{"issue":"20","key":"5127_CR44","first-page":"1","volume":"19","author":"A Corsaro","year":"2006","unstructured":"Corsaro, A., Querzoni, L., Scipioni, S., Piergiovanni, S.T., Virgillito, A., et al.: Quality of service in publish\/subscribe middleware. Global Data Manag. 19(20), 1\u201322 (2006)","journal-title":"Global Data Manag."},{"key":"5127_CR45","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.: Formalizing hybrid systems with Event-B and the rodin platform. Sci. Comput. Program. 94, 164\u2013202 (2014)","journal-title":"Sci. Comput. Program."},{"key":"5127_CR46","volume-title":"The B-book Assigning Programs to Meanings","author":"J Abrial","year":"2005","unstructured":"Abrial, J.: The B-book Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"issue":"6","key":"5127_CR47","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447\u2013466 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0145-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"4","key":"5127_CR48","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, B.R.: A ranking chaos algorithm for dual scheduling of cloud service and computing resource in private cloud. Comput. Ind. 64(4), 448\u2013463 (2013). https:\/\/doi.org\/10.1016\/j.compind.2013.02.008","journal-title":"Comput. Ind."},{"issue":"21","key":"5127_CR49","doi-asserted-by":"publisher","first-page":"8944","DOI":"10.3390\/s23218944","volume":"23","author":"FJ Jaime","year":"2023","unstructured":"Jaime, F.J., Mu\u00f1oz, A., Rodr\u00edguez-G\u00f3mez, F., Jerez-Calero, A.: Strengthening privacy and data security in biomedical microelectromechanical systems by IoT communication security and protection in smart healthcare. Sensors 23(21), 8944 (2023)","journal-title":"Sensors"},{"key":"5127_CR50","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, A., Ma\u00f1a, A., Serrano, D.: Avispa in the validation of ambient intelligence scenarios. In: 2009 International Conference on Availability, Reliability and Security, pp. 420\u2013426. IEEE (2009)","DOI":"10.1109\/ARES.2009.80"}],"container-title":["Cluster Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-025-05127-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10586-025-05127-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10586-025-05127-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T17:41:34Z","timestamp":1757439694000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10586-025-05127-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,31]]},"references-count":50,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["5127"],"URL":"https:\/\/doi.org\/10.1007\/s10586-025-05127-0","relation":{},"ISSN":["1386-7857","1573-7543"],"issn-type":[{"type":"print","value":"1386-7857"},{"type":"electronic","value":"1573-7543"}],"subject":[],"published":{"date-parts":[[2025,7,31]]},"assertion":[{"value":"8 July 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 December 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 January 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no relevant conflict of interests pertaining to the content of this study.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"445"}}