Bogor Tutorial at PLDI 2005

Model Checking Concurrent Object-Oriented Systems with Bogor
An Extensible Software Model Checking Framework for Domain-Specific Model Checking

Presenters: Dr. Robby and Dr. John Hatcliff, Kansas State University

Bogor Project Web Site: http://bogor.projects.cis.ksu.edu

Abstract:

Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. We believe that for model checking technology to be effectively applied to software, model checking tools must directly support language constructs found in modern object-oriented languages like Java and C# and underlying checking algorithms must make use of sophisticated analyses similar to those found in optimizing compilers to reduce model checking costs. Moreover, recent trends in both the requirements for software systems and the processes by which systems are developed suggest that domain-specific model checking engines may be more effective than general purpose model checking tools.

The Bogor model checking framework is an extensible and highly modular explicit-state model checking framework that aims to overcome limitations of existing model checking tools that fail to provide direct support modeling software, and to enable more effective incorporation of domain knowledge into verification models and associated model checking algorithms and optimizations.

Bogor Tree-based Counter Example Display

Bogor Graph-based Counter Example Display

This four hour tutorial will cover the following topics related to Bogor's design principles, graphical user interface and visualizations, internal architecture and APIs, working with architectural elements to create customized domain-specific model-checking engines, and example deployments of Bogor in large scale development/verification environments.

Bogor Overview: An introduction to the challenges of model checking modern multi-threaded object-oriented systems, Bogor's overarching philosophy for addressing these challenges, and illustrations of the primary capabilities of Bogor via its Eclipse-based user interface
Bogor Architecture -- Designing for OO Support and Extensibility: An overview of the internal architecture of Bogor focusing on its rationale for (a) supporting the complexities of checking highly dynamic concurrent object-oriented systems and (b) for enabling customization of core algorithms/representations and adding new constructs to Bogor's modeling language via the Bogor extension mechanism.
Customizing Bogor -- Building Your Own Domain Specific Model Checker: Step-by-step illustrations of how to easily add new domain-specific commands/expressions to Bogor's modeling language and how to increase model checking effectiveness by tailoring Bogor's internal algorithms to the characteristics of a particular domain.
Bogor Applications -- Bogor Deployed in Large-Scale Software Development Tools: Examples of how Bogor has been customized/extended to form the core model checking engine of several robust software development tools including the Cadena model-driven development environment for component-based real-time distributed systems, and the next generation of the Bandera tool set for model checking concurrent Java software. This will include a discussion of how a variety of forms of program analysis (including blends of static and dynamic alias and escape analysis) are used to drive state representation and state-space reduction strategies.

Bogor is freely distributed in an open-source format, and a variety of forms of supporting documentation and example repositories can be found on the project web-site http://bogor.projects.cis.ksu.edu.

Presenter Biography Information

Robby

Assistant Professor
SAnToS Laboratory
Department of Computing and Information Sciences
Kansas State University

Web: http://www.cis.ksu.edu/~robby

John Hatcliff

Professor
SAnToS Laboratory
Department of Computing and Information Sciences
Kansas State University

Web: http://www.cis.ksu.edu/~hatcliff

Dr. Robby (Assistant Professor at Kansas State University) and Dr. John Hatcliff (Professor at Kansas State University) together with Dr. Matthew Dwyer (Henson Professor of Engineering at University of Nebraska, Lincoln) have led the development of a variety of verification and analysis tools including the Bogor software model checking framework, the Cadena integrated development environment for component-based distributed systems, and the Bandera tool set for model checking concurrent Java programs. Their work on these tools has been supported by a variety of funding agencies including the U.S. National Science Foundation, U.S. Army Research Office (ARO), the U.S. Defence Advanced Research Projects Agency (DARPA), NASA, and by IBM, Lockheed Martin, Rockwell Collins, and Intel.