Automatic verification system based on automaton theory

Author

Yamane, Satoshi

Author_Institution

Dept. of Comput. Sci., Shimane Univ., Matsue, Japan

fYear

1996

fDate

15-16 Apr 1996

Firstpage

256

Lastpage

259

Abstract

It is important to formally verify real-time systems. The author specifies system specification and verification properties using a timed automaton. In order to avoid the state-space explosion, the author proposes the following methods. (1) Computing SCC (strongly connected components) satisfying acceptance conditions by checking timing constraints. (2) Computing SCC by image computation based on a BDD (binary decision diagram). The author has developed the verification system and demonstrated its effectiveness using the CSMA/CD protocol

Keywords

automata theory; carrier sense multiple access; formal specification; formal verification; real-time systems; timing; CSMA/CD protocol; acceptance conditions; automatic verification system; automaton theory; binary decision diagram; image computation; real-time systems; strongly connected components; system specification; timed automaton; timing constraint checking; Automata; Boolean functions; Clocks; Costs; Data structures; Explosions; Real time systems; Safety; State-space methods; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel and Distributed Real-Time Systems, 1996. Proceedings of the 4th International Workshop on

Conference_Location

Honolulu, HI

Print_ISBN

0-8186-7515-2

Type

conf

DOI

10.1109/WPDRTS.1996.557693

Filename

557693