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.
Y. S. Huang and T. C. Row, "Modelling and Verification of Vending Machine Systems by Using Timed Petri Nets", Key Engineering Materials, Vols. 467-469, pp. 1668-1673, 2011