@article{ParekhWODES24,
title = {Automatic Conversion of Smart Contracts for Non-Blocking Verification},
journal = {IFAC-PapersOnLine},
volume = {58},
number = {1},
pages = {282-287},
year = {2024},
note = {17th IFAC Workshop on discrete Event Systems WODES 2024},
issn = {2405-8963},
doi = {https://doi.org/10.1016/j.ifacol.2024.07.048},
url = {https://www.sciencedirect.com/science/article/pii/S2405896324001265},
author = {Nishant Parekh and Wolfgang Ahrendt and Martin Fabian},
keywords = {Extended finite state machines, smart contracts, security, Verification, non-blocking},
abstract = {Smart contracts are programs stored on a blockchain ledger, thus being immutable after deployment, which makes assessment of their correctness before deployment vital. Extended finite state machines (EFSM) offer a structured framework for modeling complex systems, thus providing a systematic approach to scrutinize smart contract functionalities. This paper describes a methodology to automatically convert from the abstract syntax tree of a smart contract to an EFSM model. A smart contract implementing a casino is the specific use case, and verification of the EFSM model reveals it to be blocking. This blocking represents that a malicious player can lock the funds of the casino so that they can never be retrieved.}
}