Tuesday, November 19, 2002
1:30 pm - 5:00 pm

Software Model Checking

Matthew B. Dwyer
Department of Computing and Information Sciences
Kansas State University

Abstract

Model checking is an algorithmic technique for exhaustively checking the behavioral conformance of a state transition system with a specification of its temporal behavior. Tools that automate model checking of hardware designs have become a useful component of commercial development processes. Recent years have witnessed a significant push to apply model checking technology to reason about properties of software systems. In this tutorial,

• we outline some of the major challenges to model checking modern software systems,
  
  
• we describe some of the major research efforts in the area and how they address those challenges, and
  
  
• we discuss connections between software model checking and more traditional program analysis techniques.
  

While the presentation will provide a broad overview of software model checking research, it will also go into some depth in its description of the Bandera tool set. Bandera is an integrated collection of program analysis, transformation, and visualization components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input Java source code and a software requirement formalized in Bandera's temporal specification language, and it generates a program model and specification in the input language of one of several existing model-checking tools (including Spin, dSpin, SMV, and JPF). Both program slicing and user extensible abstract interpretation components are applied to customize the program model to the property being checked. When a model-checker produces an error trail, Bandera renders the error trail at the source code level and provides a number of facilities for visualizing the path of the trail through the source code while displaying values of variables and internal states of Java lock objects.

The presentation will be supplemented by demonstrations of the application of the tools to non-trivial concurrent Java programs.

For more information on Bandera visit: http://www.cis.ksu.edu/bandera

Presenter Biography

Matthew B. Dywer is an Associate Professor in the Department of Computing and Information Sciences at Kansas State University. He co-directs work on the Bandera project which is developing an open tool platform for applying model checking techniques to software design notations and source code. Prior to joining Kansas State in 1995, he completed his PhD at the University of Massachusetts at Amherst; in his dissertation work he developed FLAVERS which applies program flow analysis techniques to reason about application specific safety properties. His interests in automated program analysis were kindled by his experiences as a Senior Engineer with Intermetrics. Inc. from 1985 through 1990. He worked on a variety of embedded system development projects, which were a rich source of subtle concurrency related bugs, and developed a range of software development tools, including source level debuggers, code generators, and the global optimizer for a family of C compilers. He received the MS in Computer Science in 1989 from the Unversity of Massachusetts at Boston and the BS in Electrical Engineering in 1985 from the University of Rochester.