Symbolic CTL Model Checking for Incomplete Designs by Selecting Property-Specific Subsets of Local Component Assumptions.
Christian Miller, Tobias Nopper, Christoph Scholl · 2009
Black Box symbolic model checking is a method to check whether an incompletely specified circuit, in which some parts of the design have been replaced by ‘Black Boxes’, satisfies a CTL property regardless of the actual replacement of the Black Boxes. One possible application is model checking with abstraction where complex parts of the design (which are not really relevant for the property at hand) are put into Black Boxes in order to speed up the model checking run. However, due to its approximative nature, symbolic model checking for incomplete designs may be unable to provide proofs when the approximations are to coarse. In this paper we show how Black Box model checking can profit from information about the Black-Boxed parts given in form of so-called local component assumptions. The assumptions we use in this context are safety properties arguing about fixed time windows. Furthermore we will present a set of heuristic-based approaches to automatically select a subset of local component assumptions that is sufficient to prove or disprove a given CTL property. 1