Filter-based model checking of partial systems
- 1 November 1998
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 23 (6) , 189-202
- https://doi.org/10.1145/288195.288307
Abstract
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.Keywords
This publication has 17 references indexed in Scilit:
- The model checker SPINIEEE Transactions on Software Engineering, 1997
- Model checking large software specificationsACM SIGSOFT Software Engineering Notes, 1996
- Evaluating deadlock detection methods for concurrent softwareIEEE Transactions on Software Engineering, 1996
- Model checking software systemsACM SIGSOFT Software Engineering Notes, 1995
- A concurrency analysis tool suite for Ada programsACM Transactions on Software Engineering and Methodology, 1995
- Data flow analysis for verifying properties of concurrent programsACM SIGSOFT Software Engineering Notes, 1994
- State-based model checking of event-driven system requirementsIEEE Transactions on Software Engineering, 1993
- Automated analysis of concurrent systems with the constrained expression toolsetIEEE Transactions on Software Engineering, 1991
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- Synthesis of Communicating Processes from Temporal Logic SpecificationsACM Transactions on Programming Languages and Systems, 1984