3rd Estonian Summer School in
Computer and Systems Science (ESSCaSS'04)

III Eesti Arvuti- ja Süsteemiteaduse Suvekool (EASTS'04)

Pedase, August 8-12, 2004.


Speaker: John Hatcliff
SAnToS Laboratory, Kansas State University


State-space exploration strategies such as model checking are emerging as a popular technology for reasoning about behavioral properties of a wide variety of software artifacts including: requirements models, architectural descriptions, designs, implementations, and process models. The computational costs of model checking are well-known, and a decade of intensive research on general techniques for reducing the complexity of model checking has made model checking tools much more efficient. Yet, past experience has shown that domain-specific information can often be leveraged to obtain state-space reductions that go beyond general purpose reductions by customizing existing model checker implementations or by building new model-checking engines dedicated to a particular domain. Unfortunately, these strategies limit the dissemination of model checking techniques across a number of domains since it is often infeasible for domain experts to build their own dedicated model checkers or to modify existing model checking engines.

To enable researchers to more easily tailor a model checking engine to a particular software-related domain, we have constructed an extensible and modular explicit-state software model checking framework called Bogor. For treating realistic designs and implementations in widely-used languages such as Java and C#, Bogor provides a rich base modeling language including features that allow for dynamic creation of objects and threads, garbage collection, virtual method calls and exception handling. For these built-in features, Bogor employs state-of-the-art reduction techniques such as collapse compression, heap symmetry, thread symmetry, and partial-order reductions that leverage common heap and locking structures. For tailoring to specific domains, Bogor provides (a) mechanisms for extending Bogor's modeling language with new primitive types, commands, expressions, and APIs associated with a particular application, and (b) a well-organized module facility for plugging customized domain-tailored components into the model-checking engine. Moreover, Bogor is designed to be easily encapsulated within larger domain-specific development and verification environments.

The goals of this series of lectures are to provide students with on overview of the foundations of explicit-state model checking as implemented by Bogor, and then to illustrate how Bogor can be customized to a particular domain.

Lecture I: Bogor Overview and Foundations of Explicit-State Model-checking

This lecture begins with an overview of the motivation for Bogor and gives a short demonstration of Bogor's input language and user interface. This is followed by an introduction to the basic concepts of explicit-state model-checking. Emphasis is placed on the primary data structures involved in the model-checker's depth-first search, as these are the data structures that one deals with when extending Bogor's input language or customizing internal modules of Bogor.

Lecture II: Writing Bogor Extensions -- A Tutorial

A simple set example is used to illustrate how Bogor's input language can be extended with new types, new expressions, and new commands. Also illustrated are the application programming interfaces (APIs) for the primary data structures of Bogor's state-space exploration engine.

Lecture III: Checking Java Programs and JML Specifications

This lecture will describe how Bogor supports model-checking of Java programs and rich specifications written in the Java Modeling Language (JML). This gives insight into how the sophisticated features of a high-level language such as methods, inheritance, exceptions, etc. can be supported in Bogor, and how Bogor's reduction strategies (e.g., partial-order reductions) are tailored to features specific of the state of object-oriented software execution such as heap and locking structures. If time permits, this lecture will also briefly survey the Bandera Temporal Specification Patterns system that a number of researchers and practitioners have found useful for constructing temporal logic specifications.

Lecture IV: Designing Component-based Systems in Cadena and Checking Cadena Designs in Bogor

This lecture gives an overview of Cadena -- a integrated development environment that we have built for the design, analysis, and implementation of systems built using the CORBA Component Model. Cadena is currently being used by research engineers at several companies including Boeing and Lockheed-Martin to demonstrate the effectiveness of model-driven component-based product-line development for avionics and command-and-control systems. Cadena uses Bogor to model-check high-level system designs, and this lecture describes how Bogor's input language and underlying state-space exploration algorithms were customized to directly support the CORBA real-time event channel middleware infrastructure used in mission- and command-control applications.

At http://www.cis.ksu.edu/santos/esscass04/ students can find materials specifically associated with these lectures including

  • the distribution of Bogor which includes user manual, tutorials, Bogor source code, and API documentation, and
  • electronic versions of lecture slides, supplementary lecture notes, guided exercises, and associated research papers for background reading.

Valid CSS! Valid XHTML 1.0 Strict Last modified on August 05 2004 21:39:41. esscass04 at cc.ioc.ee