IEEE/ICACT20210216 Slide.15        [Big Slide]       Oral Presentation
And, property 4 is a safety property. It means that the bid is delivered to the beneficiary. At this time, in the above property, it was assumed that the beneficiary initial asset is 0. property 5 is the liveness property, indicating that the contract will be terminated someday when the contract is deployed. The UPPAAL model checker was used to confirm that the model satisfies the above properties derived from the functional requirements

[Go to Next Slide]
Select Voice: