{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T17:57:38Z","timestamp":1772906258818,"version":"3.50.1"},"reference-count":145,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100003093","name":"Ministry of Higher Education Malaysia and Universiti Putra Malaysia","doi-asserted-by":"publisher","award":["FRGS\/1\/2015\/ICT01\/UPM\/02\/6"],"award-info":[{"award-number":["FRGS\/1\/2015\/ICT01\/UPM\/02\/6"]}],"id":[{"id":"10.13039\/501100003093","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2021]]},"DOI":"10.1109\/access.2021.3081742","type":"journal-article","created":{"date-parts":[[2021,5,19]],"date-time":"2021-05-19T20:50:20Z","timestamp":1621457420000},"page":"77526-77544","source":"Crossref","is-referenced-by-count":10,"title":["Handling State Space Explosion in Component-Based Software Verification: A Review"],"prefix":"10.1109","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8871-6211","authenticated-orcid":false,"given":"Faranak","family":"Nejati","sequence":"first","affiliation":[{"name":"Department of Software Engineering and Information Systems, FSKTM, Universiti Putra Malaysia, Seri Kembangan, Malaysia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1719-7335","authenticated-orcid":false,"given":"Abdul Azim Abd","family":"Ghani","sequence":"additional","affiliation":[{"name":"Department of Software Engineering and Information Systems, FSKTM, Universiti Putra Malaysia, Seri Kembangan, Malaysia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5579-7382","authenticated-orcid":false,"given":"Ng Keng","family":"Yap","sequence":"additional","affiliation":[{"name":"Department of Software Engineering and Information Systems, FSKTM, Universiti Putra Malaysia, Seri Kembangan, Malaysia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Azmi Bin","family":"Jafaar","sequence":"additional","affiliation":[{"name":"Department of Software Engineering and Information Systems, FSKTM, Universiti Putra Malaysia, Seri Kembangan, Malaysia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35079-0_21"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60385-9_13"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2882568"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.advengsoft.2013.12.007"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/CEC.2007.4425083"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2924639"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2009.19"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80096-9"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/SEW.2003.1270728"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1081180.1081193"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_19"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3301326.3301348"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.asoc.2014.06.055"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_13"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45139-0_6"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2014.2330061"},{"key":"ref24","author":"appel","year":"2004","journal-title":"Modem Compiler Implementation"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_2"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_18"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2568088.2568091"},{"key":"ref100","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_4"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_20"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2018.2868897"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2019.00007"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/ISPA\/IUCC.2017.00118"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12691-3_33"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/12.537122"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/ICCSP.2014.6949915"},{"key":"ref54","first-page":"1","article-title":"Binary decision diagrams: An improved variable ordering using graph representation of Boolean functions","volume":"1","author":"prasad","year":"2006","journal-title":"Int J Comput Sci"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1613\/jair.4586"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_26"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.4236\/jcc.2014.26004"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.1991.145386"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"ref5","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref8","first-page":"71","article-title":"Abstract model checking with SOFL hierarchy","author":"tian","year":"2012","journal-title":"Proc Int Workshop Structured Object-Oriented Formal Lang Method"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"ref9","first-page":"37","article-title":"Fighting state space explosion: Review and evaluation","author":"pel\u00e1nek","year":"2008","journal-title":"Proc Int Workshop Formal Methods Ind Critical Syst"},{"key":"ref46","first-page":"189","article-title":"A hybrid meta-heuristic approach to cope with state space explosion in model checking technique for deadlock freeness","volume":"8","author":"rezaee","year":"2020","journal-title":"Journal of AI and Data Mining"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/3306309.3306310"},{"key":"ref48","first-page":"1","article-title":"Limiting state space explosion of model checking using discrete event simulation: Combining DEVS and PROMELA","author":"khemiri","year":"2019","journal-title":"Proc Summer Simul Conf"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/ICSESS49938.2020.9237680"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/ICSESS47205.2019.9040772"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15234-4_22"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/3331452"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2942762"},{"key":"ref127","doi-asserted-by":"publisher","DOI":"10.1109\/RIVF.2013.6719860"},{"key":"ref126","article-title":"An algebraic theory of componentised interaction","author":"chilton","year":"2013"},{"key":"ref125","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_28"},{"key":"ref124","first-page":"92","article-title":"Assume-guarantee reasoning for safe component behaviours","author":"chilton","year":"2012","journal-title":"Proc Int'l Workshop Formal Aspects of Component Software"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0091-0"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374529"},{"key":"ref129","first-page":"5419","article-title":"Controller synthesis for interconnected systems using parametric assume-guarantee contracts","author":"al khatib","year":"2020","journal-title":"Proc Amer Control Conf (ACC)"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/3290364"},{"key":"ref128","doi-asserted-by":"publisher","DOI":"10.1049\/iet-sen.2009.0016"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2890695"},{"key":"ref76","article-title":"Bounded model checking and feature omission diversity","author":"amin alipour","year":"2016","journal-title":"arXiv 1610 08020"},{"key":"ref130","doi-asserted-by":"publisher","DOI":"10.1109\/KSE.2018.8573364"},{"key":"ref77","article-title":"Breadth-bounded model checking","author":"meulen","year":"2009"},{"key":"ref74","first-page":"825","article-title":"Satisfiability modulo theories","volume":"185","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"ref133","doi-asserted-by":"publisher","DOI":"10.1007\/s11227-008-0240-y"},{"key":"ref134","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16901-4_29"},{"key":"ref131","doi-asserted-by":"publisher","DOI":"10.1145\/3368926.3369659"},{"key":"ref78","first-page":"176","article-title":"Using partial orders to improve automatic verification methods","author":"godefroid","year":"1990","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref132","first-page":"1","article-title":"Compositional synthesis via a convex parameterization of assume-guarantee contracts","author":"ghasemi","year":"2020","journal-title":"Proc 23rd Int Conf Hybrid Syst Comput Control"},{"key":"ref79","first-page":"491","article-title":"Stubborn sets for reduced state space generation","author":"valmari","year":"1989","journal-title":"Proc Int Conf Appl Theory Petri Nets"},{"key":"ref136","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2014.60"},{"key":"ref135","first-page":"1","article-title":"Component-based design and verification in X-MAN","author":"he","year":"2012","journal-title":"Proc Embedded Real Time Softw Syst"},{"key":"ref138","doi-asserted-by":"publisher","DOI":"10.2514\/6.2015-1868"},{"key":"ref137","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.06.011"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"ref139","doi-asserted-by":"publisher","DOI":"10.1145\/2304736.2304746"},{"key":"ref62","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Adv Comput"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_8"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref64","article-title":"Marking pocket states for bounded on-the-fly model checking","author":"spijkerman","year":"0"},{"key":"ref140","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0410-8"},{"key":"ref65","first-page":"359","article-title":"Planning as satisfiability","volume":"92","author":"kautz","year":"1992","journal-title":"Proc ECAI"},{"key":"ref141","doi-asserted-by":"publisher","DOI":"10.1145\/2465449.2465456"},{"key":"ref66","volume":"1","author":"van harmelen","year":"2008","journal-title":"Handbook of Knowledge Representation"},{"key":"ref142","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2810807"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_3"},{"key":"ref143","doi-asserted-by":"publisher","DOI":"10.18517\/ijaseit.10.4.10179"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1145\/2693208.2693240"},{"key":"ref144","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.3004262"},{"key":"ref2","first-page":"26","article-title":"Volume II: Technical concepts of component-based software engineering","author":"bachmann","year":"2000"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2016-1310"},{"key":"ref145","first-page":"1","article-title":"A software component model and its preliminary formalisation","volume":"7","author":"lau","year":"2005","journal-title":"Formal Methods for Components and Objects \ufffd"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.70726"},{"key":"ref109","doi-asserted-by":"publisher","DOI":"10.1201\/9781420082807"},{"key":"ref95","author":"cormen","year":"2009","journal-title":"Introduction to Algorithms"},{"key":"ref108","first-page":"123","author":"pnueli","year":"1985","journal-title":"In Transition from Global to Modular Temporal Reasoning about Programs"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808746"},{"key":"ref107","doi-asserted-by":"publisher","DOI":"10.1145\/123186.123223"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028741"},{"key":"ref106","first-page":"49","article-title":"Symbolic model checking with partitioned transition relations","volume":"7","author":"burch","year":"1991","journal-title":"CiteSeer"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_19"},{"key":"ref105","doi-asserted-by":"publisher","DOI":"10.21236\/ADA339195"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.3390\/app10113928"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.1109\/AITC.2019.8920978"},{"key":"ref90","first-page":"349","article-title":"Coverage preserving reduction strategies for reachability analysis","volume":"6","author":"holzmann","year":"2013","journal-title":"Proc 12th IFIP WG"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.11"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14977-6_16"},{"key":"ref111","doi-asserted-by":"publisher","DOI":"10.5120\/908-1286"},{"key":"ref112","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"ref110","first-page":"1","article-title":"State compression in spin: Recursive indexing and compression training runs","author":"holzmann","year":"1997","journal-title":"Proc 3rd Int Spin workshop"},{"key":"ref98","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_12"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24732-6_7"},{"key":"ref96","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380180203"},{"key":"ref97","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1023\/A:1008696026254","article-title":"An analysis of bitstate hashing","volume":"13","author":"holzmann","year":"1998","journal-title":"Formal Methods System Design"},{"key":"ref10","first-page":"1379","article-title":"A survey on coping with the state space explosion problem in model checking","volume":"4","author":"rafe","year":"2013","journal-title":"International Journal of Basic & Applied Science"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3385634.3385638"},{"key":"ref12","article-title":"A classification of model checking-based verification approaches for software models","author":"gabmeyer","year":"2013","journal-title":"Proc 2nd Int Work Verification Model Transformation (VOLT)"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_44"},{"key":"ref14","first-page":"1","article-title":"Model checking and the state explosion problem","author":"clarke","year":"2011","journal-title":"LASER Summer School Software Engineering"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"ref118","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146250"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592781"},{"key":"ref82","article-title":"An approach to the state explosion problem","author":"mcmillan","year":"1992"},{"key":"ref117","doi-asserted-by":"publisher","DOI":"10.1049\/iet-sen.2009.0011"},{"key":"ref17","article-title":"A case study on model checking and deductive verification techniques of safety-critical software","author":"silva","year":"2012"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040315"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00262-2"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"ref119","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348253"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICNSC.2016.7478980"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_1"},{"key":"ref114","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380230704"},{"key":"ref113","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_32"},{"key":"ref116","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45306-7_21"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_34"},{"key":"ref115","doi-asserted-by":"publisher","DOI":"10.1145\/1103845.1094836"},{"key":"ref120","first-page":"45","article-title":"Deciding liveness in component-based systems is NP-hard","volume":"6","author":"martens","year":"2006","journal-title":"Manuskripte\/Reihe Informatik"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"ref121","author":"minnameier","year":"2006","journal-title":"Deadlock-detection component-based System is NP-hard"},{"key":"ref122","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_17"},{"key":"ref123","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0436-0"},{"key":"ref85","first-page":"156","article-title":"A stubborn attack on state explosion","author":"valmari","year":"1990","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_69"},{"key":"ref87","volume":"1","author":"robinson","year":"2001","journal-title":"'Handbook of Automated Reasoning'"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234740"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/9312710\/09435368.pdf?arnumber=9435368","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,8]],"date-time":"2022-09-08T20:48:28Z","timestamp":1662670108000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9435368\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":145,"URL":"https:\/\/doi.org\/10.1109\/access.2021.3081742","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]}}}