{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T12:12:17Z","timestamp":1781007137650,"version":"3.54.1"},"reference-count":58,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2023]]},"DOI":"10.1109\/access.2023.3325060","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T18:23:20Z","timestamp":1697480600000},"page":"115062-115075","source":"Crossref","is-referenced-by-count":37,"title":["BlockASP: A Framework for AOP-Based Model Checking Blockchain System"],"prefix":"10.1109","volume":"11","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1506-7924","authenticated-orcid":false,"given":"Anas M. R.","family":"AlSobeh","sequence":"first","affiliation":[{"name":"Department of Information Systems, Faculty of Information Technology and Computer Science, Yarmouk University, Irbid, Jordan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4513-6430","authenticated-orcid":false,"given":"Aws A.","family":"Magableh","sequence":"additional","affiliation":[{"name":"Department of Information Systems, Faculty of Information Technology and Computer Science, Yarmouk University, Irbid, Jordan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16901-4_38"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.4018\/IJWSR.2018010104"},{"key":"ref12","author":"b\u00e9rard","year":"2013","journal-title":"Systems and Software Verification Model-Checking Techniques and Tools"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.5121\/csit.2018.81204"},{"key":"ref15","first-page":"8","article-title":"Unified conceptual model for joinpoints in distributed transactions","volume":"14","author":"alsobeh","year":"2014","journal-title":"Proc ICSE"},{"key":"ref14","first-page":"173","article-title":"TransJ: An abstract independent-framework for weaving crosscutting concern into distributed transactions","volume":"7","author":"alsobeh","year":"2016","journal-title":"Applied Computing Techniques"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2023.103290"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.5455\/jjcit.71-1579451674"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1504\/IJCAT.2019.101181"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2957660"},{"key":"ref55","first-page":"1","article-title":"Architectural aspect-aware design for IoT applications: Conceptual proposal","volume":"10","author":"alsobeh","year":"2018","journal-title":"Int J Comput Sci Inf Technol"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2003.1241372"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-33743-7_44"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_29"},{"key":"ref16","first-page":"59","article-title":"Transaction-aware aspects with TransJ: An initial empirical study to demonstrate improvement in reusability","volume":"2016","author":"alsobeh","year":"2016","journal-title":"ICSEA"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3586033"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.5121\/ijsea.2018.9605"},{"key":"ref51","article-title":"Engineering blockchain based software systems: Foundations, survey, and future directions","author":"fahmideh","year":"2021","journal-title":"arXiv 2105 01881"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.3005519"},{"key":"ref46","first-page":"1","article-title":"An aspect-oriented with BIP components for better crosscutting concerns modernization in IoT applications","author":"alsobeh","year":"2018","journal-title":"Proc Comput Sci Inf Technol"},{"key":"ref45","first-page":"185","article-title":"Improving reuse of distributed transaction software with transaction-aware aspects","volume":"2","author":"alsobeh","year":"2015","journal-title":"ProQuest"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1504\/IJWMC.2018.091147"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2134243.2134246"},{"key":"ref42","first-page":"23","article-title":"Making aspect oriented system evolution safer","author":"toledano","year":"2006","journal-title":"Proc ECOOP Workshop Reflection AOP Meta-Data Softw Evol"},{"key":"ref41","first-page":"1","article-title":"Model checking for aspect-oriented software evolution","author":"ruanthong","year":"2005","journal-title":"Proc 4th WSEAS Int Conf Softw Eng Parallel Distrib Syst"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-009-9269-5"},{"key":"ref43","article-title":"A practical method for software model checking using AOP","author":"koga","year":"2012"},{"key":"ref49","first-page":"61801","article-title":"From analysis to design of the observation pattern","volume":"51","author":"yoder","year":"2017","journal-title":"Urbana"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.3390\/pr6090167"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.21533\/pen.v7i4.975"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1093\/aob\/mcr121"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.3390\/app12042016"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2022.3143145"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.jksuci.2022.03.007"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1080\/08982112.2019.1692139"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1504\/IJCAET.2012.046635"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.23919\/ICACT51234.2021.9370462"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-09843-7_8"},{"key":"ref37","first-page":"265","article-title":"Partial-order reduction in model checking object-oriented Petri nets","author":"ce\u0161ka","year":"2003","journal-title":"Computer Aided Systems Theory&#x2014;EUROCAST"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2004.1401320"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC54236.2022.00248"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ASYU56188.2022.9925532"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833721"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC54236.2022.00020"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/s42979-020-00123-0"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.3390\/app9091736"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/508386.508405"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-C.2017.142"},{"key":"ref24","first-page":"563","article-title":"Coalition logic for specification and verification of smart contract upgrades","author":"galimullin","year":"2022","journal-title":"Proc Int Conf Princ Pract Multi-Agent Syst"},{"key":"ref23","first-page":"305","article-title":"Finding unchecked low-level calls with zero false positives and negatives in Ethereum smart contracts","author":"gill","year":"2022","journal-title":"Proc Int Symp Found Pract Secur"},{"key":"ref26","first-page":"119","article-title":"Three-valued model checking smart contract systems with trust under uncertainty","author":"alwhishi","year":"2022","journal-title":"Proc Int Conf Deep Learn Big Data Blockchain"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.jksuci.2022.08.029"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.3390\/s23084046"},{"key":"ref22","first-page":"85","article-title":"Towards a dynamic testing approach for checking the correctness of Ethereum smart contracts","author":"hammami","year":"2022","journal-title":"Proc Int Conf Risk Secur Internet Syst"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/JIOT.2023.3282732"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.3390\/electronics11193091"},{"key":"ref27","article-title":"Holistic verification of blockchain consensus","author":"bertrand","year":"2022","journal-title":"arXiv 2206 04489"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/SIN56466.2022.9970534"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/10005208\/10286488.pdf?arnumber=10286488","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T23:02:55Z","timestamp":1701385375000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10286488\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"references-count":58,"URL":"https:\/\/doi.org\/10.1109\/access.2023.3325060","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]}}}