Ordering method for reducing state space in compositional verification

Author

Lee, Wan Bok ; Kim, Tag Gon

Author_Institution

Dept. of Electr. Eng., Korea Adv. Inst. of Sci. & Technol., Taejon, South Korea

Volume

1

fYear

1999

fDate

1999

Firstpage

806

Abstract

Proposes an efficient ordering method for solving the state explosion problem in compositional verification of discrete event systems. A system to be verified is specified by untimed DEVS (discrete event system specification) formalism. The size of the intermediate state space during the compositional verification is dependent on the sequence of composing system components. Application of this method to some classical verification problems has shown that the size of the intermediate state space during composition is markedly reduced

Keywords

calculus of communicating systems; concurrency control; discrete event simulation; discrete event systems; formal verification; state-space methods; compositional verification; ordering method; state explosion problem; state space reduction; untimed discrete event system specification; Computational modeling; Discrete event systems; Explosions; Manufacturing; Partial differential equations; Safety; Space technology; State-space methods; System recovery;

fLanguage

English

Publisher

ieee

Conference_Titel

Systems, Man, and Cybernetics, 1999. IEEE SMC '99 Conference Proceedings. 1999 IEEE International Conference on

Conference_Location

Tokyo

ISSN

1062-922X

Print_ISBN

0-7803-5731-0

Type

conf

DOI

10.1109/ICSMC.1999.814195

Filename

814195