A modular verification of complex real-time systems

Author

Borusan, Alexander

Author_Institution

Fachbereich Inf., Hamburg Univ., Germany

Volume

2

fYear

1994

fDate

2-5 Oct 1994

Firstpage

1308

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ICSMC.1994.400026

Filename

400026