**Propel: Tools and Methods for Practical Software Model Checking**

Massoud Mansouri-Samani

Peter Mehlitz

*Computer Sciences Corporation*

*NASA Ames Research Center*

[*massoud@email.arc.nasa.gov*](mailto:massoud@email.arc.nasa.gov)

*pcmehlitz@email.arc.nasa.gov*

Lawrence Markosian

Owen O'Malley

*QSS Group*

*NASA Ames Research Center*

*zaven@email.arc.nasa.gov owen@email.arc.nasa.gov*

Dale Martin

Lantz Moore

*Clifton Labs, Inc.*

[*dmartin@cliftonlabs.com*](mailto:dmartin@cliftonlabs.com)

[*lmoore@cliftonlabs.com*](mailto:lmoore@cliftonlabs.com)

John Penix

*Computational Sciences Division*

*NASA Ames Research Center*

[*john.penix@nasa.gov*](mailto:john.penix@nasa.gov)

Willem Visser

*Reseach Institute for Advanced Computer Science*

*NASA Ames Research Center*

*wvisser@email.arc.nasa.gov*

**Abstract**

This paper describes the development of practical model checking tools
for verification of multithreaded Java and C++ software. Our strategy is
to develop and evaluate both a design methodology that enables the
application of model checking technology and a model checking toolset.
The design concept, Design for Verification (D4V), is an adaptation of
existing "best design practices" toward the explicit goal of enhancing
verifiability by improving modularity and decreasing "accidental"
complexity. We believe that D4V can enhance a variety of V&V approaches;
we are developing the concept in the context of model checking. The
model checking toolset builds upon Java PathFinder, and explicit-stat
model checker for Java, by adding extensions to support C++. This work
involves building a translator from C++ to Java, productizing JPF, and
evaluating the toolset in the context of D4V. Throughout development, we
are evaluating Propel capabilities on NASA mission applications.

**1. Introduction**

The design concept that we are developing is Design for Verification
(D4V). This is an adaption of existing "best design practices" that has
the desired side-effect of enhancing verifiability by improving
modularity and decreasing "accidental" complexity. D4V, we believe,
enhances the applicability of a variety of V&V approaches; we are
developing the concept in the context of model checking.

The model checking toolset, Propel, is based on extending JPF to handle
C++. Our principal tasks in developing the toolset are to build a
translator from C++ to Java, productize JPF, and evaluate the toolset in
the context of D4V. Through all these tasks we are testing Propel
capabilities on customer applications.

**2. Design for Verification**

Real applications typically exceed the capabilities of today\'s V&V
tools in terms of size and complexity. As a result, these applications
often need to be manually translated into tool-specific models---an
expensive process that comes with a potential for introducing fidelity
problems. This effectively renders V&V a one-time effort inconsistent
with the evolutionary nature of large-scale system development.

As part of Propel, we are creating a methodology that explicitly adds
V&V goals to the design phase. Our purpose is to turn V&V into a
development co-process by mapping key system properties to dedicated,
separately checkable design components. This is achieved mainly by using
domain-specific design pattern systems, where each pattern instance has
its own set of tool-supported usage checks and guarantees. These, in
turn, are used to identify suitable pattern candidates based on the
system specification.

The whole application design is centered around three concepts:
Extension Points (base classes with overridable methods, delegation
objects/types), Conceptual Branch Points (potentially blocking
operations), and Check Points (consistent states that require
verification in terms of reachability and evaluation).

The methodology can be seen as an adaption of existing "best design
practices", with the desired side-effect of improving modularity and
decreasing "accidental" complexity.

The initial target defect classes for Propel are deadlocks and race
conditions, with additional properties including temporal logic
properties to be identified from Design for Verification concept
development.

**3. Translating C++ to Java**

To leverage the existing JPF model checker, we are building an automated
translator from C++ to Java. The much simpler and better-defined
semantics of Java lend themselves to be model-checked more easily and
correctly. We considered defining a new virtual machine to support C++,
rather than using Java VM in JPF, but by using the standard JVMs we can
use the large collection of tools that support Java manipulation and
verification.

Naturally, the tradeoff is that some parts of C++, such as multiple
inheritance and the loose type model, are difficult to represent in
Java. Therefore, the translated system is more complex than the original
system. Part of the ongoing research is focused on understanding and
minimizing the impact of this translation overhead on verification.

The translator is implemented with an Edison Design Group-based C++
parser, which we extended to create an XML-based abstract syntax tree
(AST). Various tree-based transformations to replace the non-Java-like
parts of C++ with Java equivalents are then applied to the AST and,
finally, Java code is published from the AST.

**4. JPF Productization**

To evaluate the capability of model-checking technology on real
applications, the tools themselves must be robust and scalable.
Therefore, we are putting significant effort into extending JPF for
faithfulness to real JVMs; refactoring the system to improve
maintainability, extensibility and testability; and implementing
performance enhancements to reduce the number of states stored, the size
of the state representation, and execution time.

For example, we have implemented a mechanism to abstract components of a
target system so that they can be partly executed in the underlying JVM
instead of entirely in the JPF JVM. This is especially important for
implementing system library abstractions that try to minimize the
relevant state space of the verified system. It also supports
extensibility of JPF by greatly simplifying the process of adding
support for system libraries that are required for real applications.

We are also enhancing usability and are planning to integrate JPF with
development environments. We have identified and are addressing
engineering risks and their mitigations, and we have identified research
issues as well. Examples of engineering or research issues include:
rendering the JPF output in a way that supports traceability and
debugging; model checking applications that have large or complex
environments that cannot be modeled adequately in JPF; and handling
concurrency libraries that are too low-level to model in JPF.

In addition to the tasks described above, we need to address technical
marketing questions such as how model checking is best integrated with
other V&V approaches, and how significantly the limitations on our
approach (or more generally on model checking) affect the set of
suitable applications of interest to NASA. Thus an important activity
for us is characterizing the relevant attributes of suitable
applications (those that increase risk or enhance applicability of our
tools), obtaining NASA mission applications (both C++ and Java),
analyzing these applications, and testing our tools with them. We are in
the process of developing collaborations with NASA missions to provide
early feedback using the productized JPF on their Java applications and
to use their Java and C++ applications to focus our product development.

We are also interested in exploring the question of return on investment
of applying model checking, but we have encountered difficulty finding
data to support a baseline ROI estimate.

**References**

\[1\] W. Visser, K. Havelund, G. Brat, S. Park. Model Checking Programs.
Proceedings of the 15th International Conference on Automated Software
Engineering (ASE), Grenoble, France, September 2000.