Induction and Model Checking

Abstract

This chapter deals with the verification of systems that are generated out of similar or identical finite state components, using a simple rule. Systems of this type are commonplace — they occur in bus protocols and network protocols, I/O channels, and many other structures that are designed to be extensible by adding similar components. In particular, we are interested in verifying properties that hold independent of the number of components in the system. We may for example have used a model checker to verify some property of a multiprocessor with a fixed number of processors. Would that property continue to hold if we added one more processor. One hundred? One thousand? Clearly, at some point we will be unable to answer the question with the model checker alone. It would be far preferable to settle the question once and for all, regardless of the number of processors.