I'm working on several projects involving developing tools and techniques for Java program analysis/verification, model driven development of distributed systems, and applying these techniques to construct high-assurance software systems.
- Cadena --- a robust tool environment for modeling, analysis, and model-driven development of large-scale distributed systems built using component middleware frameworks such as the CORBA Component Model (CCM) or Enterprise Java Beans (EJB)
- Bogor --- a customizable/extensible model-checker for object-oriented software emphasizing the notion of domain-specific model-checking
- Indus --- a featureful program slicer and static analysis framework for Java
- Bandera --- a tool suite for detecting hard-to-find defects in concurrent Java software using model-checking techniques
All of the tools above are implemented in IBM's Eclipse platform, and they've been used by a number of different academic and industrial research groups.
For more details about these tools, you can follow the links above to the tool home pages or read the overviews given below.
Cadena---A Development Environment for Design, Analysis, and Verification of Component-based Systems
The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding rapidly. Even in real-time safety/mission-critical domains, component-based development is beginning to take hold as a mechanism for incorporating non-functional aspects such as real-time, quality-of-service, and distribution.
To form an effective basis for the development of such systems, we have built Cadena---an integrated environment for building and modeling CCM systems. Cadena provides the following capabilities:
- A collection of light-weight specification forms that can be attached to CCM's component Interface Definition Language (IDL) to specify mode variable domains, intra-component dependencies, and component state-transition semantics. These forms have a natural refinement order so that useful feedback can be obtained with little annotation effort, and increasing the precision of annotation yields more precise analysis. In addition, Cadena specifications allow developers to specify the same information in different ways, achieving a form of checkable redundancy that is useful for exposing design flaws.
- Dependency analysis capabilities allow tracing inter/intra-component event and data dependencies, as well as algorithms for synthesizing dependency-based real-time and distribution aspect information.
- A component assembly framework supporting a variety of visualization and programming tools for developing component connections.
- Integration with both C++ and Java CCM implementations including CIAO (a C++ implementation built on top of the ACE/TAO real-time CORBA implementation) and OpenCCM (a Java implementation that runs on top of a number of open source Java ORBs).
- A novel model-checking infrastructure dedicated to event-based inter-component communication via real-time middleware enables system design models (derived from CCM IDL, component-assembly descriptions and annotations) to be model-checked for global system properties.
- Java component stub and skeleton code generated using the CCM IDL compilers of OpenCCM or CIAO.
The Cadena tools are implemented as plug-ins to IBM's Eclipse IDE. This provides an end-to-end integrated development environment for CCM-based Java systems moving from editing of component definitions and connections information to editing and debugging of auto-generated code templates.
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. We are actively collaborating with researchers at the University of Vanderbilt (developers of CIAO) to more effectively support model-driven development of distributed real-time embedded systems.
Bogor---An Extensible and Modular Software Model Checker
Modern computing applications increasingly require concurrent/distributed software systems that are extremely reliable. Unfortunately, current software validation techniques, such as inspections and testing, are failing to provide high levels of assurance of correctness for these systems due to system size and complexity as well as the fundamental difficulties of reasoning about state/event sequences in concurrent behavior. Model-checking techniques (now widely used for hardware verification) hold promise for establishing crucial behavioral properties of complex software because they can automatically check to see if an abstract finite-state transition system model of the software conforms to a given state/event sequence property. If the model fails to satisfy the property, the model-checker gives a counterexample --- a path through the model's transitions that violates the property. This can be used to locate and correct the corresponding software defect. Essentially, model checking performs an exhaustive simulation that captures the behavior of all possible thread interleavings in the system model being analyzed.
The promise of model checking technology for finding defects due to unanticipated interleavings in highly concurrent systems has led a number of international corporations and government research labs such as Microsoft, IBM, Lucent, NEC, NASA, and Jet Propulsion Laboratories (JPL) to fund their own software model checking projects. We believe that there are a number of trends both in the requirements of computing systems and in the processes by which they are developed that will drive persons and organizations interested in applying model checking technology to rely increasingly on customization/adaptation of existing tool frameworks or construction of new model checking tools tailored to particular domains. Moreover, past experience has shown that software model checking engines need to provide direct support for features of modern programming languages in order to effectively deal with software systems.
To address these trends, we have built Bogor -- an extensible software model checking framework with state of the art software model checking algorithms, visualizations, and user interface designed to support both general purpose and domain-specific software model checking. Although there are many model checkers available, Bogor provides a number novel capabilities that make it especially well-suited for checking properties of a variety of modern software artifacts, for building domain-specific model checking engines, and for supporting teaching of model checking concepts.
- Direct support of features found in concurrent object-oriented languages such as dynamic creation of threads and objects, object inheritance, virtual methods, exceptions, garbage collection, etc.
- Bogor's modeling language can be extended with new primitive types, expressions, and commands associated with a particular domain (e.g, multi-agent systems, avionics, security protocols, etc.) and a particular level of abstraction (e.g., design models, source code, byte code, etc.).
- Bogor's open architecture and well-organized module facility allows new algorithms (e.g., for state-space exploration, state storage, etc) and new optimizations (e.g., heuristic search strategies, domain-specific scheduling, etc.) to be easily swapped in to replace Bogor's default model checking algorithms.
- Bogor has a robust feature-rich graphical interface implemented as a plug-in for Eclipse -- an open source and extensible universal tool platform from IBM. This user interface provides mechanisms for collecting and naming different Bogor configurations, specification property collections, and a variety of visualization and navigation facilities.
- Bogor is an excellent pedagogical vehicle for teaching foundations and applications of model checking because it allows students to see clean implementations of basic model checking algorithms and to easily enhance and extend these algorithms in course projects.
In short, Bogor aims to be not only a robust and feature-rich software model checking tool that handles the language constructs found in modern large-scale software system designs and implementations, it also aims to be a model checking framework that enables researchers and engineers to create families of domain-specific model checking engines. Bogor is currently being used in a number of research projects outside of Kansas State including University of Massachusetts-Amherst, University of Nebraska-Lincoln, Brigham Young University, Queens University, and EPFL.