Title :
Automatic verification system based on automaton theory
Author_Institution :
Dept. of Comput. Sci., Shimane Univ., Matsue, Japan
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;
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
DOI :
10.1109/WPDRTS.1996.557693
