{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:27:13Z","timestamp":1740122833396,"version":"3.37.3"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,9,14]],"date-time":"2021-09-14T00:00:00Z","timestamp":1631577600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,9,14]],"date-time":"2021-09-14T00:00:00Z","timestamp":1631577600000},"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":["Multimed Tools Appl"],"published-print":{"date-parts":[[2022,1]]},"DOI":"10.1007\/s11042-021-11301-4","type":"journal-article","created":{"date-parts":[[2021,9,14]],"date-time":"2021-09-14T05:02:46Z","timestamp":1631595766000},"page":"615-636","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Trustworthy smart city systems using refinement and Event-B Theories"],"prefix":"10.1007","volume":"81","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0412-7127","authenticated-orcid":false,"given":"Eman H.","family":"Alkhammash","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,9,14]]},"reference":[{"issue":"[6]","key":"11301_CR1","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R, Butler M, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in event-b. Int J Softw Tools Technol Transfer 12([6]):447\u2013466","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"11301_CR2","doi-asserted-by":"crossref","unstructured":"Abrial JR (2010) Modeling in Event-B - system and software engineering. Cambridge University Press","DOI":"10.1017\/CBO9781139195881"},{"key":"11301_CR3","unstructured":"Alkhammash E (2014) Towards a systematic process for modelling complex systems in event-B. PhD thesis, University of Southampton"},{"key":"11301_CR4","doi-asserted-by":"crossref","unstructured":"Alkhammash E (2020) Formal modelling of owl ontologies-based requirements for the development of safe and secure smart city systems. Soft Comput:1\u201314","DOI":"10.1007\/s00500-020-04688-z"},{"key":"11301_CR5","doi-asserted-by":"crossref","unstructured":"Alkhammash EH, Butler MJ, Cristea C (2017) 15 modeling guidelines of freertos in event-b Shaping the future of ICT: trends in information technology, communications engineering and management","DOI":"10.1201\/9781315155241-15"},{"key":"11301_CR6","unstructured":"Barry R (2010) Using the freeRTOS Real Time Kernel - a Practical Guide Lulu"},{"key":"11301_CR7","unstructured":"Butler CM, Maamria I (2010) Mathematical extension in Event-B through the rodin theory component. University of Southampton"},{"key":"11301_CR8","doi-asserted-by":"crossref","unstructured":"Fu C, Zheng K (2018) Patterns for modeling task-level timing constraints with event-b. In: 218 IEEE 9th International Conference on Software Engineering and Service Science (ICSESS). IEEE, pp 260\u2013 266","DOI":"10.1109\/ICSESS.2018.8663926"},{"key":"11301_CR9","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1016\/j.future.2017.03.029","volume":"83","author":"MS Hossain","year":"2018","unstructured":"Hossain MS, Muhammad G, Abdul W, Song B, Gupta BB (2018) Cloud-assisted secure video transmission and sharing framework for smart cities. Futur Gener Comput Syst 83:596\u2013606","journal-title":"Futur Gener Comput Syst"},{"key":"11301_CR10","doi-asserted-by":"crossref","unstructured":"Iliasov A, Troubitsyna E, Laibinis L, Romanovsky A, Varpaaniemi K, Ilic D, Latvala T (2010) Developing mode-rich satellite software by refinement in event b. In: International Workshop on Formal Methods for Industrial Critical Systems. Springer, pp 50\u201366","DOI":"10.1007\/978-3-642-15898-8_4"},{"key":"11301_CR11","doi-asserted-by":"crossref","unstructured":"Iqbal Z, Khan MI (2018) Automatic incident detection in smart city using multiple traffic flow parameters via v2x communication. Int J Distrib Sensor Netw 14[11]:1550147718815845","DOI":"10.1177\/1550147718815845"},{"issue":"[1]","key":"11301_CR12","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1186\/s40294-018-0056-4","volume":"6","author":"A Jarrar","year":"2018","unstructured":"Jarrar A, Balouki Y (2018) Formal modeling of a complex adaptive air traffic control system. Compl Adapt Syst Model 6([1]):6","journal-title":"Compl Adapt Syst Model"},{"key":"11301_CR13","doi-asserted-by":"crossref","unstructured":"Joochim T, Snook C, Poppleton M, Gravell A (2010) Timing diagrams requirements modeling using event-b formal methods","DOI":"10.2316\/P.2010.677-028"},{"key":"11301_CR14","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1016\/j.proeng.2017.06.090","volume":"192","author":"M Lacin\u00e1k","year":"2017","unstructured":"Lacin\u00e1k M, Ristvej J (2017) Smart city, safety and security. Procedia Eng 192:522\u2013527","journal-title":"Procedia Eng"},{"key":"11301_CR15","doi-asserted-by":"crossref","unstructured":"Latif S, Afzaal H, Rehman A, Zafar NA (2018) Deterministic formal modeling of smart lightening system using internet of things. In: 2018 12th International Conference on Mathematics, Actuarial Science, Computer Science and Statistics (MACS). IEEE, pp 1\u20136","DOI":"10.1109\/MACS.2018.8628463"},{"key":"11301_CR16","doi-asserted-by":"crossref","unstructured":"Latif S, Afzaal H, Zafar NA (2018) Intelligent traffic monitoring and guidance system for smart city. In: 2018 International Conference on Computing, Mathematics and Engineering Technologies (icoMET). IEEE, pp 1\u20136","DOI":"10.1109\/ICOMET.2018.8346327"},{"key":"11301_CR17","doi-asserted-by":"crossref","unstructured":"Latif S, Afzaal H, Zafar NA (2018) Modelling of graph-based smart parking system using internet of things. In: 2018 International Conference on Frontiers of Information Technology (FIT). IEEE, pp 7\u201312","DOI":"10.1109\/FIT.2018.00009"},{"key":"11301_CR18","doi-asserted-by":"crossref","unstructured":"Latif S, Ferzund J (2019) Smart airport apron management system formal modeling using vdm-sl. In: 2019 13th International Conference on Mathematics, Actuarial Science, Computer Science and Statistics (MACS). IEEE, pp 1\u20136","DOI":"10.1109\/MACS48846.2019.9024825"},{"key":"11301_CR19","doi-asserted-by":"crossref","unstructured":"Latif S, Rehman A, Zafar NA (2018) Modeling of sewerage system linking uml, automata and tla+. In: 2018 International Conference on Computing, Electronic and Electrical Engineering (ICE Cube). IEEE, pp 1\u20136","DOI":"10.1109\/ICECUBE.2018.8610971"},{"key":"11301_CR20","doi-asserted-by":"crossref","unstructured":"Latif S, Rehman A, Zafar NA (2019) Blockchain and iot based formal model of smart waste management system using tla+. In: 2019 International Conference on Frontiers of Information Technology (FIT). IEEE, pp 304\u20133045","DOI":"10.1109\/FIT47737.2019.00064"},{"issue":"[3]","key":"11301_CR21","first-page":"32","volume":"8","author":"C Li","year":"2018","unstructured":"Li C, Zhang Z, Zhang L (2018) A novel authorization scheme for multimedia social networks under cloud storage method by using ma-cp-abe. Int J Cloud Appl Comput (IJCAC) 8([3]):32\u201347","journal-title":"Int J Cloud Appl Comput (IJCAC)"},{"key":"11301_CR22","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1016\/j.ins.2018.02.060","volume":"479","author":"D Li","year":"2019","unstructured":"Li D, Deng L, Gupta BB, Wang H, Choi C (2019) A novel cnn based security guaranteed image watermarking generation scenario for smart city applications. Inf Sci 479:432\u2013447","journal-title":"Inf Sci"},{"key":"11301_CR23","doi-asserted-by":"crossref","unstructured":"Li Q, Yao C (2003) Real-Time Concepts for embedded systems. CMP Books","DOI":"10.1201\/9781482280821"},{"issue":"[2]","key":"11301_CR24","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s10009-015-0391-0","volume":"19","author":"A Mammar","year":"2017","unstructured":"Mammar A, Laleau R (2017) Modeling a landing gear system in event-b. Int J Softw Tools Technol Transfer 19([2]):167\u2013186","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"11301_CR25","doi-asserted-by":"crossref","unstructured":"Predut S-N, Ipate F, Gheorghe M, Campean F (2018) Formal modelling of cruise control system using event-b and rodin platform. In: IEEE 20th International Conference on High Performance Computing and Communications; 2018 IEEE 16th International Conference on Smart City; IEEE 4th International Conference on Data Science and Systems (HPCC\/SmartCity\/DSS), pages 1541\u20131546. IEEE","DOI":"10.1109\/HPCC\/SmartCity\/DSS.2018.00253"},{"key":"11301_CR26","doi-asserted-by":"crossref","unstructured":"Rehman A, Latif S, Zafar NA (2018) Non-deterministic formal modeling of registration system towards smart campus. In: 2018 12th International Conference on Mathematics, Actuarial Science, Computer Science and Statistics (MACS). IEEE, pp 1\u20136","DOI":"10.1109\/MACS.2018.8628373"},{"key":"11301_CR27","doi-asserted-by":"crossref","unstructured":"Ristvej J, Lacin\u00e1k M, Ondrejka R (2020) On smart city and safe city concepts. Mob Netw Appl:1\u201310","DOI":"10.1007\/s11036-020-01524-4"},{"key":"11301_CR28","doi-asserted-by":"crossref","unstructured":"Romanovsky A, Thomas M (2013) Industrial deployment of system engineering methods. Springer","DOI":"10.1007\/978-3-642-33170-1"},{"issue":"[6]","key":"11301_CR29","first-page":"1","volume":"50","author":"EFZ Santana","year":"2017","unstructured":"Santana EFZ, Chaves AP, Gerosa MA, Kon F, Milojicic DS (2017) Software platforms for smart cities Concepts, requirements, challenges, and a unified reference architecture. ACM Comput Surv (Csur) 50([6]):1\u201337","journal-title":"ACM Comput Surv (Csur)"},{"key":"11301_CR30","doi-asserted-by":"crossref","unstructured":"Singh NK, Wang H, Lawford M, Maibaum TSE, Wassyng A (2015) Stepwise formal modelling and reasoning of insulin infusion pump requirements. In: International Conference on Digital Human Modeling and Applications in Health, Safety, Ergonomics and Risk Management. Springer, pp 387\u2013398","DOI":"10.1007\/978-3-319-21070-4_39"},{"key":"11301_CR31","doi-asserted-by":"crossref","unstructured":"Tsafack N, Sankar S, Abd-El-Atty B, Kengne J, Jithin KC, Belazi A, Mehmood I, Bashir Ak, Song O-Y, El-Latif AAA (2020) A new chaotic map with dynamic analysis and encryption application in internet of health things. IEEE Access 8:137731\u2013137744","DOI":"10.1109\/ACCESS.2020.3010794"},{"key":"11301_CR32","doi-asserted-by":"crossref","unstructured":"Villanueva FJ, Santofimia MJ, Villa D, Barba J, Lopezm JC (2013) Civitas: The smart city middleware, from sensors to big data. In: 2013 Seventh International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing, pages 445\u2013450. IEEE","DOI":"10.1109\/IMIS.2013.80"}],"container-title":["Multimedia Tools and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11042-021-11301-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11042-021-11301-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11042-021-11301-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,20]],"date-time":"2022-01-20T20:33:08Z","timestamp":1642710788000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11042-021-11301-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,14]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,1]]}},"alternative-id":["11301"],"URL":"https:\/\/doi.org\/10.1007\/s11042-021-11301-4","relation":{},"ISSN":["1380-7501","1573-7721"],"issn-type":[{"type":"print","value":"1380-7501"},{"type":"electronic","value":"1573-7721"}],"subject":[],"published":{"date-parts":[[2021,9,14]]},"assertion":[{"value":"3 August 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 June 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 July 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 September 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Compliance with Ethical Standards"}},{"value":"The authors declare that they have no conflicts of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Competing interests"}}]}}