1. Automatic verification is not about proving correctness, but about finding bugs much earlier in the development of a system.
2. it is no longer feasible to shut down a malfuncitoning system in order to restore saftety, even when failure
is not life-threating, the consequences of having to replace critical
code or circuity can be economically devastating.
3. deductive verification is a time-consuming process that can be performed
only by experts who are educated in logical reasoning and have
considerable experience. the proof of a single protocol or circuit can
last days or months. consequently, use
of deductive verification is rare. it is applied to highly sensitive
systems such as security protocols, where enough resources need to be
invested to guarantee their safe usage.
4. it is important to realize that some mathematical tasks cannot be
performed by an algorithm. In particular, it shows that there cannot be
an algorithm that decides whether an aribitratry computer program
terminates. This immediately limits what can be verified automatically. In particular, correct termination of programs cannot be verified
automatically in general. Thus, most proof systems cannot be completely
automated.
5. model checking is a technique for verifying finite state concurrent
systems. One benefit of this restriction is verification can be
performed automatically. The procedure normally uses an exhaustive
search of the state space of the system to determine the truth of
specification. [MEDELING
] is to convert a design into a formalism accepted by a model checker.
This may simply be a compilation task, or may require the use of
ABSTRACTION to eliminate irrelevant or unimportant details due to
limitations on time and memory. [SPECIFICATION
] is
to state the properties that the design must satisfy. This usually done
in some logical formalism. For hardware and software systems, it's
common to use temoral logic, which can assert how the behavior of the
system evolves over time. [VERIFICATION
] is
completely automatic ideally. However, in practice it often involves
human assistance. One such manual activty is the analysis of the
verification results.
6. Although symbolic representations and the partial order reduction have
greatly increased the size of the systems that can be verified, many
realistic systems are still too large to ba handled. Four other
techniques : compositional reasoning, abstraction, symmetry, and
induction.
7. compositional
reasoning: many finite state systems are composed of multiple processes
running in parallel. The specifications for such systems can often be
decomposed into properties that describe the behavior of small parts of
the system. The formal model for the system should capture the properties that must
be considered to establish correctness. On the other hand, it should
abstract away those details that do not effect the correctness of the
checked properties but make verification more complicated. A Kripke structure consists of a set of states, a set of transitions
between states, and a function that labels each state with a set of
properties that are true in this state.
(to be continue...)