Title :
A modular verification of complex real-time systems
Author :
Borusan, Alexander
Author_Institution :
Fachbereich Inf., Hamburg Univ., Germany
Abstract :
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
Keywords :
Petri nets; flexible manufacturing systems; formal specification; large-scale systems; production engineering computing; real-time systems; architecture model; complex real-time systems; flexible manufacturing cell; formalism; functional model; hierarchical coloured Petri nets; labelled state graphs; modular verification; Communication system control; Computer aided manufacturing; Computer integrated manufacturing; Digital control; Flexible manufacturing systems; Law; Legal factors; Machining; Petri nets; Process control; Real time systems; Switches; Telephony;
Conference_Titel :
Systems, Man, and Cybernetics, 1994. Humans, Information and Technology., 1994 IEEE International Conference on
Conference_Location :
San Antonio, TX
Print_ISBN :
0-7803-2129-4
DOI :
10.1109/ICSMC.1994.400026
