An efficient specification for model checking using check-points extraction method
Chikatoshi Yamada, Yasunori Nagata · 2007
In design of complex systems, embedded systems, and other critical systems, model checking, explores a finite state space to determine whether or not a given property holds, has played an important role. However, it is inefficiency to verify the entire systems. This article considers the case where designers of systems can extract check-points easily in model checking of formal verification. Moreover, we demonstrate some verification results by SPIN and NuSMV model checking tools.