Abstraction as the key for invariant verification

Abstract

We present a methodology for constructing abstractions and refining them by analyzing counter-examples. We also present a uniform verification method that combines abstraction, model-checking and deductive verification. In particular, it shows how to use the abstract system in a deductive proof even when the abstract model does not satisfy the specification and when it simulates the concrete system with respect to a weaker notion of simulation than Milner's. © Springer-Verlag Berlin Heidelberg 2003.