Formal specification and validation of a static FIFO queue modelusing coloured Petri nets

摘要

In this paper, the authors propose the use of coloured Petri nets(CPN) as a tool for the modeling of modules in flexible manufacturingsystems (FMS), and for specifying and validating their properties. Inorder to validate the proposed modules with CPN, a formal technique forqualitative validation of the system's specifications based on theplace-invariant relationships of which CPN models is used. This workanalyzes an example of a FIFO queue, which has been taken from the fieldof FMS. It is modelled through CPN, and then assessed by means of theabove proposed formal validation technique. Parallel and simultaneousresearch work is being done by the authors, but considering other FIFOand LIFO queue cases