Modelling and Verification of Vending Machine Systems by Using Timed Petri nets

摘要

This paper focuses on the use of Deterministic timed Petri net (DTPNs) to model a coffee vending machine system. The advantage of the proposed approach is that the clear presentation of the behaviors of the coffee vending machine in terms of conditions and transitions that cause the state alternations. The analysis of the control models is performed by a state transition diagram. Then the dynamic properties of the control method will be obtained. To our knowledge, this is the first work that employs DTPNs to obtain the model of the vending machine control system.