The converse of the theorem is not true as Figure 5 illustrates. A universal property that holds in the concrete system may fail to hold in the abstract system. For example, the
property agF STOP (infinitely often STOP) holds in M, but
not in Ma. Thus, a counterexample to the property in the
abstract system may fail to be a counterexample in the
concrete system. Such counterexamples are said to be
spurious counterexamples. This leads to a verification technique called Counterexample Guided Abstraction Refinement
(CEGAR).
12 Universal properties are checked on a series of
increasingly precise abstractions of the original system.
If the property holds, then by the Property Preservation
Theorem, it must hold on the concrete system and we can
stop. If it does not hold and we get a counterexample, then
we must check the counterexample on the concrete system
in order to make sure that it is not spurious. If the counterexample checks on the concrete system, then we have
found an error and can also stop. If the counterexample is
spurious, then we use information in the counterexample
to refine the abstraction mapping and repeat the loop. The
CEGAR Loop in Figure 6 generalizes an earlier abstraction
technique for sequential circuits called the localization
reduction, which was developed by R. Kurshan.
32 CEGAR is
used in many software model checkers including the SLAM
Project at Microsoft.
1
2. 4. State Explosion Challenges for the Future
The state explosion problem is likely to remain the major
challenge in model checking. There are many directions for
future research on this problem, some of which are listed
below.
• Software model checking, in particular, combining
model checking and static analysis
• Effective model checking algorithms for real-time and
hybrid systems
• Compositional model checking of complex systems
• Symmetry reduction and parameterized model checking
• Probabilistic and statistical model checking
• Combining model checking and theorem proving
• Interpreting long counterexamples
• Scaling up even more
3. JosePh sifaKis
the Quest foR coRRectness:
chaLLenGes anD PeRsPectiVes
3. 1. Where are We today?
Verification techniques have definitely found important
applications. After the first two decades of intensive research
and development, recent years have been characterized by a
shift in focus and intensity.
figure 6. the ceGaR loop.
Initial
abstraction
Program or circuit
Abstract
model
Abstraction refinement Refinement
Verification
Model
checker
No error
or bug found
Property
holds
Counterexample
Simulation
sucessful
Simulator
Bug found