Research Interests
Allen Goldberg
My primary interest is Software Engineering, specifically software
tools to improve quality, especially for high assurance systems. The
concern for high assurance has led me to work on problems in the
intersection of software engineering and security. Broadly, I try to
approach significant problems of practical interest by from a
perspective guided by a theoretical understanding of the problem. My
current work includes program generation from high-level models, and
Runtime Verification. I view this work as a practical application of
formal methods.
My thesis, supervised by Martin Davis at Courant Institute, was on the
complexity of logics. I showed that the Davis-Putnam procedure, which
would later be extensively used for SAT-based model checkers and
constraint solvers, has polynomial average case complexity. At UCSC and
Kestrel Institute my main research focus was on generation of code from
specifications via program transformation. This includes construction
of a system (DTRE) for data type specification (by defining abstract
data types as logical theories), and transformation based on theory
interpretation. DTRE was extended with a hierarchical state machine
model (REACTO), and used by NSA to specify high-assurance systems.
Other worked concerned high-level control structure transformations
such as loop fusion (deforestation), caching and dynamic programming,
derivation reuse, theorem proving, high-level program analysis, and
derivation of parallel programs. I managed a project sponsored for
Boeing in which a theorem prover was used to determine control path
feasibility of avionics software. This information in turn was used to
determine the feasibility of MCDC test requirements. In the area of
language-based security I analyzed the Java byte code verifier, giving
a formal specification and using it to find three bugs the Sun JDK. In
follow up work we formalized Java class loading and proved a type
safety result. In other security related work I, with colleagues from
Motorola, specified a separation kernel.
I have consulted for industry including work in databases, web
services, and structured multi-dimensional and text search.
My current work on enabling the use of Java on NASA
spacecraft. I have developed a domain specific language (DSL) for
flight software based on the JPL MDS system, and the translation
of the DSL into a sfety critical subset of Real Time Java.
Recent work has been on Runtime
Verification, a hybrid testing
and formal method assurance methodology based on monitoring the
execution of programs for conformance to properties specified in a
formal temporal logic. We have defined such a temporal logic, called Eagle, and are
working on fast algorithms that check program traces against properties
specified in the logic. We have also created tools for the automatic
instrumentation of Java programs to create traces. We have used Eagle
as part of a larger system of test case generation and test execution.
My recent work also includes using partial evaluation to generate C
code from Stateflow (Mathwork’s hierarchical state machine modeling
notation) models.
The area of Runtime
Verification is rapidly growing and there are many opportunities
for future research. I would like to continue core work on logics and
algorithms. One can integrate Runtime Verification with commonly-used
design notations to monitor code for conformance with design intent.
Runtime monitoring need not be restricted to a V&V activity, but
can become an integral part of the fielded software. This raises the
possibility of not only detecting errors in fielded software, but
analyzing the source of error and taking corrective action. This is
related to the emerging fields of autonomic computing and integrated
vehicle health management. A short white paper on this subject can be
found on my website. Just as fielded software can be monitored for
software faults; it can also be monitored for security
properties. For example, resource usage, patterns of message
traffic, and module call sequences can be monitored against expected
use profiles. We believe Eagle is well-suited for these applications.
I am also interested in V&V methods for autonomy software. Autonomy
software has the potential of expanding the capabilities of autonomous
vehicles, and reducing the need for human control of mission-critical
systems. True autonomy software, such as constraint-based planners,
utilizes heuristic algorithms that raise significant V&V issues
that require new specialized methods and processes. I have studied
these problems in working groups studying autonomy insertion for future
Mars Rover missions and have applied Run Time Verification to the
activity planner used on NASA’s Mars MER mission. I am an organizer of
a workshop on Verification and Validation of Model-Based Planning and
Scheduling Systems, part of the 2005 International Conference on
Automated Planning and Scheduling.