Prev Up Next
Go backward to Representing, Verifying, and Applying
Generic Software Development Steps Using PVS
Axel Dold

Go up to Specification and Verification
Go forward to Generic Specification and Verification
Friedrich von Henke, in collaboration with
F. Bartels, A. Dold, H. Pfeifer, H. Rueß


Filter-based Model Checking of Partial Systems
Matthew B. Dwyer and Corina S. Pasareanu

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. Success in scaling these techniques to be practical for realistic software systems has met with a number of obstacles, such as exponentially-sized state spaces and the problem of constructing finite-state system models for analysis. We describe 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 model checking techniques to individual 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.


 

Prev Up Next