{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:40:44Z","timestamp":1764873644548,"version":"3.37.3"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,9,6]],"date-time":"2019-09-06T00:00:00Z","timestamp":1567728000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,9,6]],"date-time":"2019-09-06T00:00:00Z","timestamp":1567728000000},"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":["Mobile Netw Appl"],"published-print":{"date-parts":[[2023,4]]},"DOI":"10.1007\/s11036-019-01369-6","type":"journal-article","created":{"date-parts":[[2019,9,6]],"date-time":"2019-09-06T06:03:26Z","timestamp":1567749806000},"page":"732-743","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Improving Formal Verification and Testing Techniques for Internet of Things and Smart Cities"],"prefix":"10.1007","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8873-9755","authenticated-orcid":false,"given":"Moez","family":"Krichen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,6]]},"reference":[{"key":"1369_CR1","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-030-13705-2_6","volume-title":"Comparison of decision trees and deep learning for object classification in autonomous driving","author":"F Alam","year":"2020","unstructured":"Alam F, Mehmood R, Katib I (2020) Comparison of decision trees and deep learning for object classification in autonomous driving. Springer International Publishing, Cham, pp 135\u2013158. https:\/\/doi.org\/10.1007\/978-3-030-13705-2_6"},{"key":"1369_CR2","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/j.procs.2016.09.068.","volume":"98","author":"F Alam","year":"2016","unstructured":"Alam F, Mehmood R, Katib I, Albeshri A (2016) Analysis of eight data mining algorithms for smarter internet of things (iot). Proc Comput Sci 98:437\u2013442. https:\/\/doi.org\/10.1016\/j.procs.2016.09.068. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S187705091632213X. The 7th International Conference on Emerging Ubiquitous Systems and Pervasive Networks (EUSPN 2016)\/The 6th International Conference on Current and Future Trends of Information and Communication Technologies in Healthcare (ICTH-2016)\/Affiliated Workshops","journal-title":"Proc Comput Sci"},{"key":"1369_CR3","doi-asserted-by":"publisher","first-page":"9533","DOI":"10.1109\/ACCESS.2017.2697839","volume":"5","author":"F Alam","year":"2017","unstructured":"Alam F, Mehmood R, Katib I, Albogami NN, Albeshri A (2017) Data fusion and iot for smart ubiquitous environments: A survey. IEEE Access 5:9533\u20139554. https:\/\/doi.org\/10.1109\/ACCESS.2017.2697839","journal-title":"IEEE Access"},{"key":"1369_CR4","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-030-13705-2_9","volume-title":"A survey of methods and tools for large-scale DNA mixture profiling","author":"E Alamoudi","year":"2020","unstructured":"Alamoudi E, Mehmood R, Albeshri A, Gojobori T (2020) A survey of methods and tools for large-scale DNA mixture profiling. Springer International Publishing, Cham, pp 217\u2013248. https:\/\/doi.org\/10.1007\/978-3-030-13705-2_9"},{"key":"1369_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1080\/10630732.2014.942092","volume":"22","author":"V Albino","year":"2015","unstructured":"Albino V, Berardi U, Dangelico R (2015) Smart cities: Definitions, dimensions, performance, and initiatives. J Urban Technol 22:3\u201321","journal-title":"J Urban Technol"},{"key":"1369_CR6","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126:183\u2013235","journal-title":"Theor Comput Sci"},{"key":"1369_CR7","doi-asserted-by":"publisher","unstructured":"Andraus ZS, Sakallah KA (2004) Automatic abstraction and verification of verilog models. In: Proceedings of the 41st annual design automation conference, DAC \u201904. ACM, New York, pp 218\u2013223. https:\/\/doi.org\/10.1145\/996566.996629","DOI":"10.1145\/996566.996629"},{"key":"1369_CR8","doi-asserted-by":"publisher","unstructured":"Aqib M, Mehmood R, Alzahrani A, Katib I, Albeshri A, Altowaijri SM (2019) Rapid transit systems: Smarter urban planning using big data, in-memory computing, deep learning, and gpus. Sustainability 11(10). https:\/\/doi.org\/10.3390\/su11102736. https:\/\/www.mdpi.com\/2071-1050\/11\/10\/2736","DOI":"10.3390\/su11102736"},{"key":"1369_CR9","doi-asserted-by":"publisher","unstructured":"Aqib M, Mehmood R, Alzahrani A, Katib I, Albeshri A, Altowaijri SM (2019) Smarter traffic prediction using big data, in-memory computing, deep learning and gpus Sensors 19(9). https:\/\/doi.org\/10.3390\/s19092206","DOI":"10.3390\/s19092206"},{"issue":"1","key":"1369_CR10","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2009.08.004.","volume":"250","author":"L Benalycherif","year":"2009","unstructured":"Benalycherif L, McIsaac A (2009) A semantic condition for data independence and applications in hardware verification. Electron Notes Theor Comput Sci 250(1):39\u201354. https:\/\/doi.org\/10.1016\/j.entcs.2009.08.004. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066109003296. Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS 2007)","journal-title":"Electron Notes Theor Comput Sci"},{"key":"1369_CR11","unstructured":"Bensalem S, Krichen M, Majdoub L, Robbana R, Tripakis S (2007) A simplified approach for testing real-time systems based on action refinement. In: ISoLA, Revue des Nouvelles Technologies de l\u2019Information, vol. RNTI-SM-1, pp. 191\u2013202. C\u0117padu\u0117s-\u0116ditions"},{"key":"1369_CR12","unstructured":"Bertot Y, Castran P (2010) Interactive theorem proving and program development: Coq\u2019Art the calculus of inductive constructions, 1st edn, Springer Publishing Company, Incorporated"},{"key":"1369_CR13","doi-asserted-by":"crossref","unstructured":"Bornot S, Sifakis J, Tripakis S (1998) Modeling urgency in timed systems. In: Compositionality, LNCS, vol 1536. Springer","DOI":"10.1007\/3-540-49213-5_5"},{"issue":"6","key":"1369_CR14","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S Chaki","year":"2004","unstructured":"Chaki S, Clarke EM, Groce A, Jha S, Veith H (2004) Modular verification of software components in c. IEEE Trans Softw Eng 30(6):388\u2013402. https:\/\/doi.org\/10.1109\/TSE.2004.22","journal-title":"IEEE Trans Softw Eng"},{"key":"1369_CR15","doi-asserted-by":"publisher","unstructured":"Lee C-C, Jiang JR, Huang C-Y, Mishchenko A (2007) Scalable exploration of functional dependency by interpolation and incremental sat solving. In: 2007 IEEE\/ACM international conference on computer-aided design, pp 227\u2013233, DOI https:\/\/doi.org\/10.1109\/ICCAD.2007.4397270","DOI":"10.1109\/ICCAD.2007.4397270"},{"key":"1369_CR16","doi-asserted-by":"crossref","unstructured":"Clarke EM, Emerson EA (1982) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs, workshop. Springer-Verlag, Berlin, pp 52\u201371. http:\/\/dl.acm.org\/citation.cfm?id=648063.747438","DOI":"10.1007\/BFb0025774"},{"key":"1369_CR17","doi-asserted-by":"crossref","unstructured":"Emerson EA, Wahl T (2005) Dynamic symmetry reduction. In: Halbwachs N, Zuck LD (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 382\u2013396","DOI":"10.1007\/978-3-540-31980-1_25"},{"volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","year":"1993","key":"1369_CR18","unstructured":"Gordon MJC, Melham TF (eds) (1993) Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, New York"},{"key":"1369_CR19","doi-asserted-by":"crossref","unstructured":"Hessel A, Larsen K, Nielsen B, Pettersson P, Skou A (2003) Time-optimal real-time test case generation using UPPAAL. In: FATES\u201903","DOI":"10.1007\/978-3-540-24617-6_9"},{"key":"1369_CR20","doi-asserted-by":"publisher","unstructured":"Hu AJ, Dill DL (1993) Reducing bdd size by exploiting functional dependencies. In: 30th ACM\/IEEE design automation conference, pp 266\u2013271. https:\/\/doi.org\/10.1145\/157485.164888","DOI":"10.1145\/157485.164888"},{"key":"1369_CR21","doi-asserted-by":"crossref","unstructured":"Iosif R (2002) Symmetry reduction criteria for software model checking. In: Bo\u0161na\u010dki D, Leue S (eds) Software, model checking. Springer, Berlin, pp 22\u201341","DOI":"10.1007\/3-540-46017-9_5"},{"key":"1369_CR22","unstructured":"Ip CN (1998) Generalized reversible rules. In: Proceedings of the 2nd international conference on formal methods in computer-aided design, FMCAD \u201998. Springer-Verlag, London, pp 403\u2013420. http:\/\/dl.acm.org\/citation.cfm?id=646185.758715"},{"key":"1369_CR23","doi-asserted-by":"publisher","unstructured":"Ip CN, Dill DL State reduction using reversible rules. In: Proceedings of the 33st Conference on Design Automation, Las Vegas, Nevada, USA, Las Vegas Convention Center, June 3-7, 1996., pp 564\u2013567 1996. https:\/\/doi.org\/10.1145\/240518.240625","DOI":"10.1145\/240518.240625"},{"key":"1369_CR24","doi-asserted-by":"crossref","unstructured":"Jiang JHR, Brayton RK (2004) Functional dependency for verification reduction. In: Alur R, Peled DA (eds) Computer aided verification. Springer, Berlin, pp 268\u2013280","DOI":"10.1007\/978-3-540-27813-9_21"},{"key":"1369_CR25","doi-asserted-by":"crossref","unstructured":"Kesten Y, Pnueli A, Zlatu\u0161ka J (1998) Modularization and abstraction: The keys to practical formal verification. In: Brim L, Gruska J (eds) Mathematical foundations of computer science 1998. Springer, Berlin, pp 54\u201371","DOI":"10.1007\/BFb0055757"},{"issue":"1\/2","key":"1369_CR26","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1504\/IJCCBS.2012.045075","volume":"3","author":"M Krichen","year":"2012","unstructured":"Krichen M (2012) A formal framework for black-box conformance testing of distributed real-time systems. IJCCBS 3(1\/2):26\u201343. https:\/\/doi.org\/10.1504\/IJCCBS.2012.045075","journal-title":"IJCCBS"},{"key":"1369_CR27","doi-asserted-by":"crossref","unstructured":"Krichen M, Cheikhrouhou O, Lahami M, Alroobaea R, Jmal Ma\u00e2lej A. (2018) Towards a model-based testing framework for the security of internet of things for smart city applications. In: Mehmood R, Bhaduri B, Katib I, Chlamtac I (eds) Smart societies, infrastructure, technologies and applications. Springer International Publishing, Cham, pp 360\u2013365","DOI":"10.1007\/978-3-319-94180-6_34"},{"issue":"3\/4","key":"1369_CR28","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1504\/IJCCBS.2018.096437","volume":"8","author":"M Krichen","year":"2018","unstructured":"Krichen M, Ma\u00e2lej AJ, Lahami M (2018) A model-based approach to combine conformance and load tests: an ehealth case study. IJCCBS 8(3\/4):282\u2013310. https:\/\/doi.org\/10.1504\/IJCCBS.2018.096437","journal-title":"IJCCBS"},{"key":"1369_CR29","doi-asserted-by":"crossref","unstructured":"Krichen M, Tripakis S Black-box conformance testing for real-time systems. In: 11th international spin workshop on model checking of software (SPIN\u201904), LNCS, vol. 2989. Springer (2004). Available at http:\/\/www-verimag.imag.fr\/PEOPLE\/Stavros.Tripakis\/papers\/timetest.pdf","DOI":"10.1007\/978-3-540-24732-6_8"},{"issue":"3","key":"1369_CR30","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/s10703-009-0065-1","volume":"34","author":"M Krichen","year":"2009","unstructured":"Krichen M, Tripakis S (2009) Conformance testing for real-time systems. Formal Methods in System Design 34(3):238\u2013304","journal-title":"Formal Methods in System Design"},{"issue":"1963","key":"1369_CR31","first-page":"83","volume":"16","author":"SA Kripke","year":"1963","unstructured":"Kripke SA (1963) Semantical considerations on modal logic. Acta Philosophica Fennica 16(1963):83\u201394","journal-title":"Acta Philosophica Fennica"},{"key":"1369_CR32","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2006) Symmetry reduction for probabilistic model checking. In: Ball T, Jones RB (eds) Computer aided verification. Springer, Berlin, pp 234\u2013248","DOI":"10.1007\/11817963_23"},{"key":"1369_CR33","doi-asserted-by":"crossref","unstructured":"Lahami M, Fakhfakh F, Krichen M, Jma\u00efel M (2012) Towards a TTCN-3 test system for runtime testing of adaptable and distributed systems. In: Proceedings of the 24th IFIP WG 6.1 international conference testing software and systems (ICTSS\u201912), pp 71\u201386","DOI":"10.1007\/978-3-642-34691-0_7"},{"key":"1369_CR34","doi-asserted-by":"publisher","unstructured":"Lahami M, Krichen M, Barhoumi H, Jmaiel M (2015) Selective test generation approach for testing dynamic behavioral adaptations. In: Testing software and systems - 27th IFIP WG 6.1 International Conference, ICTSS 2015, Sharjah and Dubai, United Arab Emirates, November 23-25, 2015, Proceedings, pp 224\u2013239. https:\/\/doi.org\/10.1007\/978-3-319-25945-1_14","DOI":"10.1007\/978-3-319-25945-1_14"},{"key":"1369_CR35","doi-asserted-by":"crossref","unstructured":"Lahami M, Krichen M, Bouchakwa M, Jma\u00efel M (2012) Using knapsack problem model to design a resource aware test architecture for adaptable and distributed systems. In: Proceedings of the 24th IFIP WG 6.1 international conference testing software and systems (ICTSS\u201912), pp. 103\u2013118","DOI":"10.1007\/978-3-642-34691-0_9"},{"key":"1369_CR36","unstructured":"Maa\u0307lej AJ, Lahami M, Krichen M, Jma\u00efel M (2018) Distributed and resource-aware load testing of WS-BPEL compositions. In: ICEIS (2), pp. 29\u201338. SciTePress"},{"key":"1369_CR37","doi-asserted-by":"publisher","first-page":"1107","DOI":"10.1016\/j.procs.2015.08.566","volume":"64","author":"R Mehmood","year":"2015","unstructured":"Mehmood R, Graham G (2015) Big data logistics: A health-care transport capacity sharing model. Proc Comput Sci 64:1107\u20131114. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1877050915027015. Conference on ENTERprise Information Systems\/International Conference on Project MANagement\/Conference on Health and Social Care Information Systems and Technologies, CENTERIS\/ProjMAN \/ HCist 2015 October 7\u20139, 2015, https:\/\/doi.org\/10.1016\/j.procs.2015.08.566","journal-title":"Proc Comput Sci"},{"key":"1369_CR38","doi-asserted-by":"publisher","unstructured":"Mehmood R, Katib I, Chlamtac I, Bhaduri B (2018) Smart societies, infrastructure, technologies and applications: First international conference, SCITA 2017, Jeddah, Saudi Arabia, November 27\u201329, 2017, Proceedings, Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering book series (LNICST, volume 224) Springer. https:\/\/doi.org\/10.1007\/978-3-319-94180-6","DOI":"10.1007\/978-3-319-94180-6"},{"issue":"6","key":"1369_CR39","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2005.04.003","volume":"128","author":"L Momtahan","year":"2005","unstructured":"Momtahan L (2005) Towards a small model theorem for data independent systems in alloy. Electron Notes Theor Comput Sci 128(6):37\u201352. https:\/\/doi.org\/10.1016\/j.entcs.2005.04.003. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066105002355. Proceedings of the Fouth International Workshop on Automated Verification of Critical Systems (AVoCS 2004)","journal-title":"Electron Notes Theor Comput Sci"},{"key":"1369_CR40","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/978-3-030-13705-2_25","volume-title":"HCDSR: A hierarchical clustered fault tolerant routing technique for IoT-based smart societies","author":"T Muhammed","year":"2020","unstructured":"Muhammed T, Mehmood R, Albeshri A, Alzahrani A (2020) HCDSR: A hierarchical clustered fault tolerant routing technique for IoT-based smart societies. Springer International Publishing, Cham, pp 609\u2013628. https:\/\/doi.org\/10.1007\/978-3-030-13705-2_25"},{"key":"1369_CR41","doi-asserted-by":"publisher","first-page":"32258","DOI":"10.1109\/ACCESS.2018.2846609","volume":"6","author":"T Muhammed","year":"2018","unstructured":"Muhammed T, Mehmood R, Albeshri A, Katib I (2018) Ubehealth: A personalized ubiquitous cloud and edge-enabled networked healthcare system for smart cities. IEEE Access 6:32258\u201332285. https:\/\/doi.org\/10.1109\/ACCESS.2018.2846609","journal-title":"IEEE Access"},{"key":"1369_CR42","unstructured":"Myers G (1979) The art of software testing. Wiley"},{"key":"1369_CR43","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/S0065-2458(10)80002-6","volume":"80","author":"ACD Neto","year":"2010","unstructured":"Neto ACD, Travassos GH (2010) A picture from the model-based testing area: Concepts, techniques, and challenges. Adv Comput 80:45\u2013120","journal-title":"Adv Comput"},{"key":"1369_CR44","doi-asserted-by":"crossref","unstructured":"Nielsen B, Skou A (2001) Automated test generation from timed automata. In: TACAS\u201901. LNCS 2031, Springer","DOI":"10.1007\/3-540-45319-9_24"},{"key":"1369_CR45","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic, LNCS, vol 2283. Springer","DOI":"10.1007\/3-540-45949-9"},{"issue":"1","key":"1369_CR46","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"DL Dill","year":"1996","unstructured":"Norris IPC, Dill DL (1996) Better verification through symmetry. Formal Methods in System Design 9 (1):41\u201375. https:\/\/doi.org\/10.1007\/BF00625968","journal-title":"Formal Methods in System Design"},{"key":"1369_CR47","doi-asserted-by":"crossref","unstructured":"Queille JP, Sifakis J (1982) Specification and verification of concurrent systems in cesar. In: Proceedings of the 5th colloquium on international symposium on programming. http:\/\/dl.acm.org\/citation.cfm?id=647325.721668. Springer-Verlag, London, pp 337\u2013351","DOI":"10.1007\/3-540-11494-7_22"},{"issue":"1","key":"1369_CR48","doi-asserted-by":"publisher","first-page":"147","DOI":"10.3233\/JCS-1999-72-303","volume":"7","author":"AW Roscoe","year":"1999","unstructured":"Roscoe AW, Broadfoot PJ (1999) Proving security protocols with model checkers by data independence techniques. J Comput Secur 7(1):147\u2013190. http:\/\/content.iospress.com\/articles\/journal-of-computer-security\/jcs120","journal-title":"J Comput Secur"},{"key":"1369_CR49","doi-asserted-by":"crossref","unstructured":"Schlingensiepen J, Mehmood R, Nemtanu FC, Niculescu M (2014) Increasing sustainability of road transport in european cities and metropolitan areas by facilitating autonomic road transport systems (arts). In: Wellnitz J, Subic A, Trufin R (eds) Sustainable automotive technologies 2013. Springer International Publishing, Cham, pp 201\u2013210","DOI":"10.1007\/978-3-319-01884-3_20"},{"key":"1369_CR50","doi-asserted-by":"crossref","unstructured":"Sifakis J, Yovine S (1996) Compositional specification of timed systems. In: 13th annual symposium on theoretical aspects of computer science, STACS\u201996, LNCS, vol 1046. Spinger-Verlag","DOI":"10.1007\/3-540-60922-9_29"},{"key":"1369_CR51","doi-asserted-by":"publisher","unstructured":"S\u00f6derstr\u00f6m O, Paasche T, Klauser F (2014) Smart cities as corporate storytelling. City: analysis of urban trends 18. https:\/\/doi.org\/10.1080\/13604813.2014.906716","DOI":"10.1080\/13604813.2014.906716"},{"key":"1369_CR52","doi-asserted-by":"crossref","unstructured":"Springintveld J, Vaandrager F, D\u2019Argenio P (2001) Testing timed automata. Theoretical Computer Science 254","DOI":"10.1016\/S0304-3975(99)00134-6"},{"key":"1369_CR53","doi-asserted-by":"publisher","unstructured":"Thacker RA, Jones KR, Myers CJ, Zheng H (2010) Automatic abstraction for verification of cyber-physical systems. In: Proceedings of the 1st ACM\/IEEE international conference on cyber-physical systems, ICCPS \u201910. ACM, New York, pp 12\u201321, DOI https:\/\/doi.org\/10.1145\/1795194.1795197","DOI":"10.1145\/1795194.1795197"},{"key":"1369_CR54","unstructured":"Tretmans J (1992) A formal approcah to conformance testing. Ph.D. thesis, University of Twente Twente The Netherlands"},{"issue":"5","key":"1369_CR55","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1002\/stvr.456","volume":"22","author":"M Utting","year":"2012","unstructured":"Utting M, Pretschner A, Legeard B (2012) A taxonomy of model-based testing approaches. Softw Test Verif Reliab 22(5):297\u2013312. https:\/\/doi.org\/10.1002\/stvr.456","journal-title":"Softw Test Verif Reliab"},{"key":"1369_CR56","doi-asserted-by":"crossref","unstructured":"Velev MN (2001) Automatic abstraction of memories in the formal verification of superscalar microprocessors. In: Margaria T, Yi W (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 252\u2013267","DOI":"10.1007\/3-540-45319-9_18"},{"issue":"2","key":"1369_CR57","doi-asserted-by":"publisher","first-page":"799","DOI":"10.3390\/sym2020799","volume":"2","author":"T Wahl","year":"2010","unstructured":"Wahl T, Donaldson A (2010) Replication and abstraction: Symmetry in automated formal verification. Symmetry 2(2):799\u2013847. https:\/\/doi.org\/10.3390\/sym2020799","journal-title":"Symmetry"},{"key":"1369_CR58","doi-asserted-by":"publisher","unstructured":"Lee W, Pardo A, Jang J-Y, Hachtel G, Somenzi F (1996) Tearing based automatic abstraction for ctl model checking. In: Proceedings of international conference on computer aided design, pp 76\u201381, DOI https:\/\/doi.org\/10.1109\/ICCAD.1996.568969","DOI":"10.1109\/ICCAD.1996.568969"},{"key":"1369_CR59","doi-asserted-by":"publisher","unstructured":"Zhang J, Goldsby HJ, Cheng BH (2009) Modular verification of dynamically adaptive systems. In: Proceedings of the 8th ACM international conference on aspect-oriented software development, AOSD \u201909. ACM, New York, pp 161\u2013172, DOI https:\/\/doi.org\/10.1145\/1509239.1509262","DOI":"10.1145\/1509239.1509262"},{"issue":"11","key":"1369_CR60","doi-asserted-by":"publisher","first-page":"1485","DOI":"10.1016\/j.infsof.2009.06.012","volume":"51","author":"H Zhu","year":"2009","unstructured":"Zhu H, Belli F (2009) Advancing test automation technology to meet the challenges of model-based software testing - guest editors\u2019 introduction to the special section of the third IEEE international workshop on automation of software test (AST 2008). Inf Softw Technol 51(11):1485\u20131486","journal-title":"Inf Softw Technol"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-019-01369-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11036-019-01369-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-019-01369-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,2]],"date-time":"2024-04-02T15:22:22Z","timestamp":1712071342000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11036-019-01369-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,6]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["1369"],"URL":"https:\/\/doi.org\/10.1007\/s11036-019-01369-6","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"type":"print","value":"1383-469X"},{"type":"electronic","value":"1572-8153"}],"subject":[],"published":{"date-parts":[[2019,9,6]]},"assertion":[{"value":"6 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}