Filter-based Model Checking of Partial Systems

Recent years have seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software, systems. Most of this work has been aimed at reasoning about properties of complete systems. This paper describes an automatable approach for building finite-state models of partially defined software systems that are amenable to model checking using existing tools. It enables the application of existing model checking tools to system components taking into account assumptions about the behavior of the environment in which the components will execute. We illustrate the application of the approach by validating and verifying properties of a reusable parameterized programming framework. 1.1 Keywords Software verification and validation, model checking, assume-guarantee reasoning, filter-based analysis 2 INTRODUCTION Modern software is, increasingly, built as a collection of independently produced c..