Filter-based model checking of partial systems

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.

REFERENCES

• 1: S. Abramsky , C. Hankin, Abstract interpretation of declarative languages, Halsted Press, New York, NY, 1987
• 2: Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.156-166, Nov. 1996
• 3: J. M. Atlee , J. Gannon, State-Based Model Checking of Event-Driven System Requirements, IEEE Transactions on Software Engineering, v.19 n.1, p.24-40, January 1993 [doi>10.1109/32.210305]
• 4: George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991 [doi>10.1109/32.106975]
• 5: George S. Avrunin , James C. Corbett , Laura K. Dillon, Analyzing partially-implemented real-time systems, Proceedings of the 19th international conference on Software engineering, p.228-238, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253275]
• 6: Shing C. Cheung , Jeff Kramer, Checking subsystem safety properties in compositional reachability analysis, Proceedings of the 18th international conference on Software engineering, p.144-154, March 25-29, 1996, Berlin, Germany
• 7: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 8: Christopher Colby , Patrice Godefroid , Lalita Jategaonkar Jagadeesan, Automatically closing open reactive programs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.345-357, June 17-19, 1998, Montreal, Quebec, Canada
• 9: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 10: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 11: M. B. Dwyer, Modular flow analysis for concurrent software, Proceedings of the 12th international conference on Automated software engineering (formerly: KBSE), p.264, November 02-05, 1997
• 12: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Property specification patterns for finite-state verification, Proceedings of the second workshop on Formal methods in software practice, p.7-15, March 04-05, 1998, Clearwater Beach, Florida, United States [doi>10.1145/298595.298598]
• 13: Matthew B. Dwyer , Vicki Carr , Laura Hines, Model checking graphical user interfaces using abstractions, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.244-261, September 22-25, 1997, Zurich, Switzerland
• 14: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.62-75, Dec. 1994
• 15: Matthew B. Dwyer , Matthew J. Craig , Eric Runquist, An application-independent concurrency skeleton in Ada 95, Proceedings of the conference on TRI-Ada '96: disciplined software development with Ada, p.179-192, December 03-07, 1996, Philadelphia, Pennsylvania, United States [doi>10.1145/240678.240715]
• 16: M. Dwyer and D. Schmidt. Limiting state explosion with filter-based refinement. In Proceedings of the 1st International Workshop on Verification, Abstract Interpretation and hiodel Checking, Oct. 1997.
• 17: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 18: J. Hat&I, M. B. Dwyer, and S. Laubach. Staging static analysis using abstraction-based program speciahzation. In Proceedings of the Joint International Symposium of the 10th Programming Languages, Implementations, Logic3 and Programs and the 7th Algebraic and Logic Programming Conferences (PLILP/ALP), Sept. 1998.
• 19: J. Hatcliff, M. B. Dwyer, S. Laubach, J. Mayans, and N. Muhammad. Automatically specializing software for finite-state verification. Technical Report 98-4, Kansas State University, Department of Computing and Information Sciences, 1998.
• 20: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 21: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 22: Orna Kupferman , Moshe Y. Vardi, Module Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.75-86, August 03, 1996
• 23: Orna Kupferman , Moshe Y. Vardi, Module Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.75-86, August 03, 1996
• 24: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 25: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 26: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 27: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 28: Gleb Naumovich , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, Applying static analysis to software architectures, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.77-93, September 22-25, 1997, Zurich, Switzerland
• 29: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 30: Jeannette M. Wing , Mandana Vaziri-Farahani, Model checking software systems: a case study, ACM SIGSOFT Software Engineering Notes, v.20 n.4, p.128-139, Oct. 1995
• 31: Pierre Wolper, Expressing interesting properties of programs in propositional temporal logic, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.184-193, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512661]
• 32: Michal Young , Richard N. Taylor , David L. Levine , Kari A. Nies , Debra Brodbeck, A concurrency analysis tool suite for Ada programs: rationale, design, and preliminary experience, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.1, p.65-106, Jan. 1995 [doi>10.1145/201055.201080]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

General Terms:
Algorithms, Design, Measurement, Performance, Reliability, Theory, Verification

Keywords:
assume-guarantee reasoning, filter-based analysis, model checking, software verification and validation