 |
The above model is a model of a Beneficiary(seller) of a smart contract-based Dutch auction system using the UPPAAL modeling tool.
First, the seller sets the auction time, the initial proposed price of the item, the lowest proposed price, the deduction amount, and the deduction time interval and distributes the smart contract.
At this time, if you enter an incorrect value, the deployment is terminated because it is an invalid smart contract.
Also, if the auction ends correctly, the contract will be terminated and it will return to the waiting state for deployment.
And, Deadlock does not occur due to time constraints in all states, and the auction ends automatically when the auction end time specified by the seller is reached. |
IEEE/ICACT20210216 Slide.10
[Big Slide]