A modular verification of complex real-time systems
Alexander Borusan · 2002
The verification technique proposed in this paper requires the construction of the labelled state graphs for the given functional model and architecture model to prove that both have the same legal trajectories regarding the same set of observables. Our tool and formalism for specifying and verifying complex real-time systems is hierarchical coloured Petri nets (CPN). We introduce two different types of CPN based real-time system models: functional model, and architecture model. To illustrate our approach, we specify and verify a flexible manufacturing cell.>