Title :
Model checking: its basics and reality
Author :
Fujita, Masahiro
Author_Institution :
Fujitsu Lab. of America, Santa Clara, CA, USA
Abstract :
Model checking is one of the most practical techniques by which we can automatically check if given specifications (properties) are satisfied by given designs. In this paper we review various verification efforts for real designs with model checking as well as a brief introduction to the algorithms relating to model checking. The goal of the paper is to give general ideas on how model checking can be applied to real designs in which way and what kind of human interaction is necessary for practical verification
Keywords :
formal specification; formal verification; temporal logic; model checking; verification efforts; Algorithm design and analysis; Automata; Formal verification; Hardware design languages; Humans; Laboratories; Logic; Natural languages; State-space methods; Timing;
Conference_Titel :
Design Automation Conference 1998. Proceedings of the ASP-DAC '98. Asia and South Pacific
Conference_Location :
Yokohama
Print_ISBN :
0-7803-4425-1
DOI :
10.1109/ASPDAC.1998.669449