Overview

Project List (Active)

Advanced Testing
The objective of the automated testing project is to perform automated generation of test inputs that obtain high coverage for flexible (user-definable) coverage metrics and to check properties of code during test case generation.
+ Visit Advanced Testing

Analysis Tools for C++
MCP is an explicit-state software model checker that supports the entire C++ programming language. In this demonstration, we will describe its architecture and present some initial results.
+ Visit Analysis Tools for C++

Applications of Neural Networks in High Assurance Systems
Since the early days of Neural Network research, the large potential for applications in many areas has been recognized and exploited. Today applications include intelligent-adaptive aircraft control, control of chemical and power plants, steel manufacturing, and financial forecasting. Nevertheless, the number of successful Neural Network applications in high assurance systems is still comparatively limited.
+ Visit Applications of Neural Networks in High Assurance Systems

C Global Surveyor
We have designed a static analyzer, called CGS, that can find runtime errors in C programs. We have successfully analyzed the flight software systems for several Mars missions (Mars pathFinder, Deep Space One, and Mars Exploration Rover).
+ Visit C Global Surveyor

Compositional Verification
Compositional verification is a promising approach to addressing the state explosion problem associated with model checking. One compositional technique advocates proving properties of a system by checking properties of its components in an assume-guarantee style. However, the application of this technique is difficult because it involves non-trivial human input. To check a component against a property, our approach generates assumptions that the environment needs to satisfy for the property to hold. These assumptions are then discharged on the rest of the system. Assumptions are computed by a learning algorithm. They are initially approximate, but become gradually more precise by means of counterexamples obtained by model checking the component and its environment, alternately
+ Visit Compositional Verification

Honeywell's DEOS Operation System
We have an ongoing collaboration with The Honeywell Technology Center to experiment with advanced verification technology for the DEOS real-time operating system for business and commuter aviation systems. We are currently experimenting with the Spin model checker and the Verisoft tool, both from Bell Labs. DEOS is written in C++ and we are interested in knowing of any tool that may be useful.
+ Visit Honeywell's DEOS Operation System

HSTS Planner Domain Models for Deep Space 1
We did a trial study of applying model checking to validate the models used in the HSTS Planner. We developed a translation from a subset of the HSTS Domain Description Language into a general model of finite-state transition systems and evaluated the translation using Spin, SMV and Murphi.
+ Visit HSTS Planner Domain Models for Deep Space 1

Java PathFinder
The majority of work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers and model checkers. We believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy we have developed a verification and testing environment for Java which integrates model checking, program analysis and testing - called Java PathFinder (JPF).
+ Visit Java PathFinder

Propel: Property Checking for C++
We are developing and evaluating several model checking and testing platforms for C++ programs. One approach translates C++ to Java and feeds it to Java PathFinder. Another approach uses the Valgrind open source tool. Another uses Aspect C++.
+ Visit Propel: Property Checking for C++

Remote Agent Executive for Deep Space 1
Using the Spin model checker, we found bugs in the intelligent plan execution software to be deployed in the Deep Space 1 spacecraft. The engineers were favorably impressed, and collaboration is continuing.
+ Visit Remote Agent Executive for Deep Space 1

Software Risk Management
The objective of this project is to identify and quantify risk factors which cause software to fail, and quantify the abilities of different V&V methods and tools to mitigate those risks. Armed with such quantification, we can determine which specific V&V tool or combination of tools will be most appropriate to effectively mitigate the risks in any specific project.
+ Visit Software Risk Management

The Livingstone Model-Based Diagnosis System
We have collaborated with the NASA Ames Autonomous Systems Group and CMU to provide model checking for the Livingstone system using the SMV model checker.
+ Visit The Livingstone Model-Based Diagnosis System

Verification and Validation of Adaptive Control Software
We have developed advanced tools and techniques for the verification and validation of adaptive control software, which represents a significant leap forward in the development of machine control systems.
+ Visit Verification and Validation of Adaptive Control Software