{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T04:53:07Z","timestamp":1749099187169,"version":"3.28.0"},"reference-count":17,"publisher":"IEEE","license":[{"start":{"date-parts":[[2022,2,13]],"date-time":"2022-02-13T00:00:00Z","timestamp":1644710400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,2,13]],"date-time":"2022-02-13T00:00:00Z","timestamp":1644710400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,2,13]]},"DOI":"10.23919\/icact53585.2022.9728854","type":"proceedings-article","created":{"date-parts":[[2022,3,11]],"date-time":"2022-03-11T20:27:02Z","timestamp":1647030422000},"page":"48-52","source":"Crossref","is-referenced-by-count":4,"title":["Formal Modeling of Smart Contract-based Trading System"],"prefix":"10.23919","author":[{"given":"Woong Sub","family":"Park","sequence":"first","affiliation":[{"name":"Korea University,School of Cybersecurity,Seoul,Republic of Korea,02841"}]},{"given":"Hyuk","family":"Lee","sequence":"additional","affiliation":[{"name":"Korea University,School of Cybersecurity,Seoul,Republic of Korea,02841"}]},{"given":"Jin-Young","family":"Choi","sequence":"additional","affiliation":[{"name":"Korea University,School of Cybersecurity,Seoul,Republic of Korea,02841"}]}],"member":"263","reference":[{"key":"ref10","article-title":"Nusmv 2: An opensource tool for symbolic model checking","author":"alessandro","year":"2002","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref12","first-page":"101","article-title":"Model checking smart contracts for Ethereum","volume":"63","author":"thomas","year":"2020","journal-title":"Pervasive and Mobile Computing"},{"key":"ref13","article-title":"Modeling bitcoin contracts by timed automata","author":"marcin","year":"2014","journal-title":"Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems"},{"year":"0","key":"ref14"},{"key":"ref15","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"clarke","year":"1981","journal-title":"Workshop on Logic of Programs"},{"key":"ref16","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/j.entcs.2009.02.044","article-title":"Model-checking timed temporal logics","volume":"231","author":"patricia","year":"2009","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"ref17","article-title":"Model-checking for real-time systems","author":"rajeev","year":"1990","journal-title":"[1990] Proceedings Fifth Annual IEEE Symposium on Logic in Computer Science"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2812844"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10916-018-0982-x"},{"journal-title":"WIRED 2016 A $50 MILLION HACK JUST SHOWED THAT THE DAO WAS ALL TOO HUMAN","year":"2016","key":"ref6"},{"key":"ref5","doi-asserted-by":"crossref","first-page":"14757","DOI":"10.1109\/ACCESS.2017.2730843","article-title":"MeDShare: Trust-less medical data sharing among cloud service providers via blockchain","volume":"5","author":"xia","year":"2017","journal-title":"IEEE Access"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"24477","DOI":"10.1109\/ACCESS.2019.2895670","article-title":"Trustworthy electronic voting using adjusted blockchain technology","volume":"7","author":"basit","year":"2019","journal-title":"IEEE Access"},{"key":"ref1","article-title":"Formalizing and securing relationships on public networks","author":"nick","year":"1997","journal-title":"First Monday"},{"key":"ref9","article-title":"Model-checking of smart contracts","author":"zeinab","year":"2018","journal-title":"2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData)"}],"event":{"name":"2022 24th International Conference on Advanced Communication Technology (ICACT)","start":{"date-parts":[[2022,2,13]]},"location":"PyeongChang Kwangwoon_Do, Korea, Republic of","end":{"date-parts":[[2022,2,16]]}},"container-title":["2022 24th International Conference on Advanced Communication Technology (ICACT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9728250\/9728768\/09728854.pdf?arnumber=9728854","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,23]],"date-time":"2022-05-23T21:29:12Z","timestamp":1653341352000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9728854\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,13]]},"references-count":17,"URL":"https:\/\/doi.org\/10.23919\/icact53585.2022.9728854","relation":{},"subject":[],"published":{"date-parts":[[2022,2,13]]}}}