{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T19:14:52Z","timestamp":1783192492995,"version":"3.54.6"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Serv Sci Res"],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1007\/s12927-019-0003-8","type":"journal-article","created":{"date-parts":[[2019,7,1]],"date-time":"2019-07-01T07:03:34Z","timestamp":1561964614000},"page":"47-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":51,"title":["A State-of-the-Art Survey on Formal Verification of the Internet of Things Applications"],"prefix":"10.1007","volume":"11","author":[{"given":"Alireza","family":"Souri","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Monire","family":"Norouzi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,6,30]]},"reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"publisher","first-page":"204","DOI":"10.3390\/su11010204","volume":"11","author":"S Ahmad","year":"2019","unstructured":"Ahmad S, Malik S, Ullah I, Park DH, Kim K, & Kim D (2019). Towards the Design of a Formal Verification and Evaluation Tool of Real-Time Tasks Scheduling of IoT Applications. Sustainability 11(1): 204.","journal-title":"Sustainability"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Aktas MS, & Astekin M (2019) Provenance aware run-time verification of things for self-healing Internet of Things applications. Concurrency and Computation: Practice and Experience, e4263-n\/a. DOI: \n                    https:\/\/doi.org\/10.1002\/cpe.4263\n                    \n                  .","DOI":"10.1002\/cpe.4263"},{"issue":"3","key":"3_CR3","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1049\/iet-com.2018.5119","volume":"13","author":"MS Ali","year":"2019","unstructured":"Ali MS, Jewel MKH, Li Y, & Lin F (2019) Frequency-domain channel equalisation for LTE-based uplink narrowband Internet of Things systems. IET Communications 13(3): 281\u2013288. \n                    https:\/\/digital-library.theiet.org\/content\/journals\/10.1049\/iet-com.2018.5119","journal-title":"IET Communications"},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jnca.2018.07.013","volume":"120","author":"P Asghari","year":"2018","unstructured":"Asghari P, Rahmani AM, & Javadi HHS (2018) Service composition approaches in IoT: A systematic review. Journal of Network and Computer Applications 120: 61\u201377. doi: \n                    https:\/\/doi.org\/10.1016\/j.jnca.2018.07.013\n                    \n                  .","journal-title":"Journal of Network and Computer Applications"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/j.comnet.2018.12.008","volume":"148","author":"P Asghari","year":"2019","unstructured":"Asghari P, Rahmani AM, & Javadi HHS (2019). Internet of Things applications: A systematic review. Computer Networks 148: 241\u2013261.","journal-title":"Computer Networks"},{"key":"3_CR6","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 Networks 36: 49\u201357.","journal-title":"Ad Hoc Networks"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Bae WS (2017) Verifying a secure authentication protocol for IoT medical devices. Cluster Computing. DOI: \n                    https:\/\/doi.org\/10.1007\/s10586-017-1107-x\n                    \n                  .","DOI":"10.1007\/s10586-017-1107-x"},{"issue":"17","key":"3_CR8","doi-asserted-by":"publisher","first-page":"2164","DOI":"10.1049\/iet-com.2018.5077","volume":"12","author":"Y Deng","year":"2018","unstructured":"Deng Y, Chen Z, Zhang D, & Zhao M (2018) Workload scheduling toward worst-case delay and optimal utility for single-hop Fog-IoT architecture. IET Communications 12(17): 2164\u20132173.","journal-title":"IET Communications"},{"issue":"5","key":"3_CR9","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1007\/s12652-016-0371-6","volume":"7","author":"V Desnitsky","year":"2016","unstructured":"Desnitsky V & Kotenko I (2016) Automated design, verification and testing of secure systems with embedded devices based on elicitation of expert knowledge. Journal of Ambient Intelligence and Humanized Computing 7(5): 705\u2013719.","journal-title":"Journal of Ambient Intelligence and Humanized Computing"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/j.jisa.2017.01.003","volume":"34","author":"PK Dhillon","year":"2017","unstructured":"Dhillon PK & Kalra S (2017a) A lightweight biometrics based remote user authentication scheme for IoT services. Journal of Information Security and Applications 34: 255\u2013270.","journal-title":"Journal of Information Security and Applications"},{"issue":"16","key":"3_CR11","doi-asserted-by":"publisher","first-page":"e3323","DOI":"10.1002\/dac.3323","volume":"30","author":"PK Dhillon","year":"2017","unstructured":"Dhillon PK & Kalra S (2017b) Secure multi-factor remote user authentication scheme for Internet of Things environments. International Journal of Communication Systems 30(16): e3323-n\/a.","journal-title":"International Journal of Communication Systems"},{"key":"3_CR12","first-page":"266","volume-title":"Dependable Software Engineering","author":"M Diwan","year":"2017","unstructured":"Diwan M & D\u2019Souza M (2017) A Framework for Modeling and Verifying IoT Communication Protocols. In K. G. Larsen, O. Sokolsky & J. Wang (Eds.), Dependable Software Engineering. Theories, Tools, and Applications: Third International Symposium, SETTA 2017, Changsha, China, Proceedings (pp. 266\u2013280). Cham: Springer International Publishing."},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Drozdov D, Patil S, Dubinin V, & Vyatkin V (2017) Towards formal verification for cyber-physically agnostic software: A case study. Paper presented at the IECON 2017 \u2014 43rd Annual Conference of the IEEE Industrial Electronics Society.","DOI":"10.1109\/IECON.2017.8216953"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-53946-1_6","volume-title":"Formal Techniques for Safety-Critical Systems: 5th International Workshop, FTSCS 2016, Tokyo, Japan, November 14, 2016","author":"M Elleuch","year":"2017","unstructured":"Elleuch M, Hasan O, Tahar S, & Abid M. (2017) Formal Probabilistic Analysis of a WSN-Based Monitoring Framework for IoT Applications. In C. Artho & P. C. \u00d6lveczky (Eds.), Formal Techniques for Safety-Critical Systems: 5th International Workshop, FTSCS 2016, Tokyo, Japan, November 14, 2016, Revised Selected Papers (pp. 93\u2013108). Cham: Springer International Publishing."},{"issue":"10","key":"3_CR15","first-page":"1865","volume":"48","author":"M Ghobaei-Arani","year":"2018","unstructured":"Ghobaei-Arani M, Rahmanian AA, Souri A, & Rahmani AM (2018) A moth-flame optimization algorithm for web service composition in cloud computing: Simulation and verification. Software: Practice and Experience, 48(10): 1865\u20131892.","journal-title":"Software: Practice and Experience"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Hameed K, Khan A, Ahmed M, Goutham Reddy A, & Rathore MM (2017) Towards a formally verified zero watermarking scheme for data integrity in the Internet of Things based-wireless sensor networks. Future Generation Computer Systems. doi: \n                    https:\/\/doi.org\/10.1016\/j.future.2017.12.009\n                    \n                  .","DOI":"10.1016\/j.future.2017.12.009"},{"issue":"4","key":"3_CR17","doi-asserted-by":"publisher","first-page":"2335","DOI":"10.1007\/s10586-016-0669-3","volume":"19","author":"KH Han","year":"2016","unstructured":"Han KH, & Bae WS (2016) Proposing and verifying a security-enhanced protocol for IoT-based communication for medical devices. Cluster Computing 19(4): 2335\u20132341.","journal-title":"Cluster Computing"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-319-58460-7_24","volume-title":"Human Aspects of Information Security, Privacy and Trust: 5th International Conference, HAS 2017, Held as Part of HCI International 2017, Vancouver, BC, Canada, July 9\u201314, 2017, Proceedings","author":"F Kamm\u00fcller","year":"2017","unstructured":"Kamm\u00fcller F (2017) Formal Modeling and Analysis with Humans in Infrastructures for IoT Health Care Systems. In T. Tryfonas (Ed.), Human Aspects of Information Security, Privacy and Trust: 5th International Conference, HAS 2017, Held as Part of HCI International 2017, Vancouver, BC, Canada, July 9\u201314, 2017, Proceedings (pp. 339\u2013352). Cham: Springer International Publishing."},{"key":"3_CR19","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-60585-2_12","volume-title":"Advances in Human Factors in Cybersecurity: Proceedings of the AHFE 2017 International Conference on Human Factors in Cybersecurity, July 17\u201321, 2017, The Westin Bonaventure Hotel, Los Angeles, California, USA","author":"F Kamm\u00fcller","year":"2018","unstructured":"Kamm\u00fcller F (2018) Human Centric Security and Privacy for the IoT Using Formal Techniques. In D. Nicholson (Ed.), Advances in Human Factors in Cybersecurity: Proceedings of the AHFE 2017 International Conference on Human Factors in Cybersecurity, July 17\u201321, 2017, The Westin Bonaventure Hotel, Los Angeles, California, USA (pp. 106\u2013116). Cham: Springer International Publishing."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Kim H, Kang E, Lee EA, & Broman D (2017) A Toolkit for Construction of Authorization Service Infrastructure for the Internet of Things. Paper presented at the 2017 IEEE\/ACM Second International Conference on Internet-of-Things Design and Implementation (IoTDI).","DOI":"10.1145\/3054977.3054980"},{"issue":"4","key":"3_CR21","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1016\/j.jcss.2015.10.007","volume":"82","author":"HJ La","year":"2016","unstructured":"La HJ (2016) A conceptual framework for trajectory-based medical analytics with IoT contexts. Journal of Computer and System Sciences 82(4): 610\u2013626.","journal-title":"Journal of Computer and System Sciences"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.ic.2018.01.001","volume":"259","author":"R Lanotte","year":"2018","unstructured":"Lanotte R & Merro M (2018) A semantic theory of the Internet of Things. Information and Computation 259: 72\u2013101.","journal-title":"Information and Computation"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-54876-0_9","volume-title":"Risks and Security of Internet and Systems: 11th International Conference, CRiSIS 2016, Roscoff, France, September 5\u20137, 2016","author":"F Mangano","year":"2017","unstructured":"Mangano F, Duquennoy S, & Kosmatov N. (2017) Formal Verification of a Memory Allocation Module of Contiki with Frama-C: A Case Study. In F. Cuppens, N. Cuppens, J.-L. Lanet & A. Legay (Eds.), Risks and Security of Internet and Systems: 11th International Conference, CRiSIS 2016, Roscoff, France, September 5\u20137, 2016, Revised Selected Papers (pp. 114\u2013120). Cham: Springer International Publishing."},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"5494","DOI":"10.1109\/ACCESS.2017.2696031","volume":"5","author":"M Mohsin","year":"2017","unstructured":"Mohsin M, Sardar MU, Hasan O, & Anwar Z (2017) IoTRiskAnalyzer: A Probabilistic Model Checking Based Framework for Formal Risk Analytics of the Internet of Things. IEEE Access 5: 5494\u20135505.","journal-title":"IEEE Access"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Nishiwaki Y (2016) F-Calculus: A Universal Programming Language of Self-Stabilizing Computational Fields. Paper presented at the 2016 IEEE 1st International Workshops on Foundations and Applications of Self* Systems (FAS*W).","DOI":"10.1109\/FAS-W.2016.51"},{"issue":"18","key":"3_CR26","doi-asserted-by":"publisher","first-page":"5943","DOI":"10.1002\/sec.1748","volume":"9","author":"A Ouaddah","year":"2016","unstructured":"Ouaddah A, Abou Elkalam A, & Ait Ouahman A (2016) FairAccess: a new Blockchain-based access control framework for the Internet of Things. Security and Communication Networks 9(18): 5943\u20135964.","journal-title":"Security and Communication Networks"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Perkovi\u0107 T, \u010cagalj M, & Kova\u010devi\u0107 T (2019) LISA: Visible light based initialization and SMS based authentication of constrained IoT devices. Future Generation Computer Systems.","DOI":"10.1016\/j.future.2019.02.052"},{"key":"3_CR28","first-page":"1","volume":"99","author":"D Saxena","year":"2017","unstructured":"Saxena D & Raychoudhury V (2017) Design and Verification of an NDN-Based Safety-Critical Application: A Case Study With Smart Healthcare. IEEE Transactions on Systems, Man, and Cybernetics: Systems 99: 1\u201315.","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics: Systems"},{"issue":"2","key":"3_CR29","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s12927-017-0011-5","volume":"9","author":"A Souri","year":"2017","unstructured":"Souri A, Asghari P, & Rezaei R (2017) Software as a service based CRM providers in the cloud computing: Challenges and technical issues. Journal of Service Science Research 9(2): 219\u2013237.","journal-title":"Journal of Service Science Research"},{"issue":"3","key":"3_CR30","first-page":"546","volume":"4","author":"A Souri","year":"2016","unstructured":"Souri A, Norouzi M, Safarkhanlou A, & Sardroud SHEH (2016) A dynamic data replication with consistency approach in data grids: modeling and verification. Baltic Journal of Modern Computing 4(3): 546.","journal-title":"Baltic Journal of Modern Computing"},{"issue":"3","key":"3_CR31","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1108\/K-02-2018-0092","volume":"48","author":"A Souri","year":"2018","unstructured":"Souri A, Nourozi M, Rahmani AM, & Jafari Navimipour N (2018a) A model checking approach for user relationship management in the social network. Kybernetes 48(3): 407\u2013423.","journal-title":"Kybernetes"},{"issue":"17","key":"3_CR32","doi-asserted-by":"publisher","first-page":"e3808","DOI":"10.1002\/dac.3808","volume":"31","author":"A Souri","year":"2018","unstructured":"Souri A, Rahmani, AM, & Jafari Navimipour N (2018b), Formal verification approaches in the web service composition: A comprehensive analysis of the current challenges for future research. International Journal of Communication Systems 31(17): e3808.","journal-title":"International Journal of Communication Systems"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Souri A, Rahmani AM, Navimipour NJ, & Rezaei, R. (2019) Formal modeling and verification of a service composition approach in the social customer relationship management system. Information Technology & People, (Earlycite) \n                    https:\/\/doi.org\/10.1108\/ITP-02-2018-0109\n                    \n                  .","DOI":"10.1108\/ITP-02-2018-0109"},{"issue":"1","key":"3_CR34","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1186\/s13673-019-0165-x","volume":"9","author":"A Souri","year":"2019","unstructured":"Souri A, Rahmani AM, Navimipour NJ, & Rezaei R (2019) A symbolic model checking approach in formal verification of distributed systems. Human-centric Computing and Information Sciences 9(1): 4. DOI: \n                    https:\/\/doi.org\/10.1186\/s13673-019-0165-x\n                    \n                  .","journal-title":"Human-centric Computing and Information Sciences"},{"key":"3_CR35","first-page":"663","volume-title":"On the Move to Meaningful Internet Systems. OTM 2017 Conferences: Confederated International Conferences: CoopIS, C&TC, and ODBASE 2017, Rhodes, Greece, October 23\u201327, 2017","author":"S Tata","year":"2017","unstructured":"Tata S, Klai K, & Jain R (2017) Formal Model and Method to Decompose Process-Aware IoT Applications. In H. Panetto, C. Debruyne, W. Gaaloul, M. Papazoglou, A. Paschke, C. A. Ardagna & R. Meersman (Eds.), On the Move to Meaningful Internet Systems. OTM 2017 Conferences: Confederated International Conferences: CoopIS, C&TC, and ODBASE 2017, Rhodes, Greece, October 23\u201327, 2017, Proceedings, Part I (pp. 663\u2013680). Cham: Springer International Publishing."},{"issue":"16","key":"3_CR36","doi-asserted-by":"publisher","first-page":"3324","DOI":"10.1002\/sec.1537","volume":"9","author":"A Venckauskas","year":"2016","unstructured":"Venckauskas A, Stuikys V, Damasevicius R, & Jusas N (2016) Modelling of Internet of Things units for estimating security-energy-performance relationships for quality of service and environment awareness. Security and Communication Networks 9(16): 3324\u20133339.","journal-title":"Security and Communication Networks"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Xu S, Miao W, Kunz T, Wei T, & Chen M (2016) Quantitative Analysis of Variation-Aware Internet of Things Designs Using Statistical Model Checking. Paper presented at the +2016 IEEE International Conference on Software Quality, Reliability and Security (QRS).","DOI":"10.1109\/QRS.2016.39"},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"27132","DOI":"10.1109\/ACCESS.2017.2766180","volume":"5","author":"S Zahra","year":"2017","unstructured":"Zahra S, Alam M, Javaid Q, Wahid A, Javaid N, Malik SUR, & Khan MK (2017) Fog Computing Over IoT: A Secure Deployment and Formal Verification. IEEE Access 5: 27132\u201327144.","journal-title":"IEEE Access"},{"issue":"17","key":"3_CR39","doi-asserted-by":"publisher","first-page":"4819","DOI":"10.1002\/cpe.3469","volume":"27","author":"Y Zhang","year":"2015","unstructured":"Zhang Y & Chen JL (2015) Constructing scalable Internet of Things services based on their event-driven models. Concurrency and Computation: Practice and Experience 27(17): 4819\u20134851.","journal-title":"Concurrency and Computation: Practice and Experience"}],"container-title":["Journal of Service Science Research"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s12927-019-0003-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s12927-019-0003-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s12927-019-0003-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,28]],"date-time":"2020-06-28T23:05:30Z","timestamp":1593385530000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s12927-019-0003-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["3"],"URL":"https:\/\/doi.org\/10.1007\/s12927-019-0003-8","relation":{},"ISSN":["2093-0720","2093-0739"],"issn-type":[{"value":"2093-0720","type":"print"},{"value":"2093-0739","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,6]]},"assertion":[{"value":"21 February 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 May 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 June 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}