Skip Navigation
About NASALatest NewsMultimediaMissionsMy NASAWork For NASA

Highlights

C Global Surveyor Used for ISS Water Recovery System Verification. May 2008.

Guillaume Brat participated in the verification of the software controlling the Water Recovery System (WRS) for the International Space Station (ISS). WRS is composed of two systems, the Water Processor Assembly (WPA) and the Urine Processor Assembly (UPA). Both systems are controlled by software developed in the C language at Marshall Space Flight Center (MSFC).Having done some static analysis on an early version of the UPA a few years ago, Brat was asked by Robert Erickson (MSFC) to analyze the latest version of the UPA code using C Global Surveyor, a static analyzer for C programs developed by Guillaume Brat and Arnaud Venet in the Robust Software Engineering group in the Intelligent Systems Division (Code TI) at NASA Ames.

Presentations [PDF, 67K]

Java Pathfinder Workshop Held. May 2008.

This year's annual Java PathFinder (JPF) workshop was held May 1– 2, 2008 at the Fujitsu Laboratories campus in Sunnyvale, CA. It was attended by participants from industry, government organizations, and academia, which came from as far as the University of Durham, UK, and the University of Tokyo, Japan. The two days were packed with talks spanning a gamut from JPF tutorials to presentations of ongoing JPF applications such as Fujitsu’s WEAVE project for model checking web applications and the new bytecode-based symbolic execution mode for JPF.

Presentations [PDF, 53K]

Course on Verification and Validation of Adaptive Systems. April 2008.

Johann Schumann
Johann Schumann of the Reliable Software Engineering (RSE) group, also a contributor to the ETDP ISD project, was invited to teach a five-day course titled Verification and Validation of Adaptive Systems as part of the ten-week lecture series Sixth Semester of UNESCO Chair: Discrete Mathematics, held in Tunis, Tunisia.

Presentations [PDF, 59K]

Model Analysis and Verification Testing Paper Accepted. April 2008.

Corina Pasareanu
One of the objectives of the Model Analysis and Verification Testing Task is to develop automated testing capabilities for mission-critical software that both measure test coverage and generate test case suites satisfying user-specified test criteria. The enabling technologies for test case generation are software model checking, symbolic execution, and constraint solving. A paper describing this work was accepted for publication at the International Symposium on Software Testing and Analysis (ISSTA’08), Seattle, WA, July 20-24 2008. The paper, “Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software,�? was co-authored by Corina Pasareanu, Peter Mehlitz, David Bushnell, Karen Gundy-Burlet, and Michael Lowry (ARC); Suzette Person (University of Nebraska-Lincoln); and Mark Pape (JSC).

Presentations [PDF, 52K]

Automated Test Case Generation Applied to PadAbort-1 Models. April 2008.

Joe Coughlan
Model analysis and test capabilities have been implemented in the Java PathFinder verification framework and have been applied to selected Simulink, Stateflow, and Embedded Matlab models of PadAbort-1 (Guidance &Navigation sub-system), resulting in test suites that guarantee full path, transition, and state coverage. A report has been written describing the work. A comparison with T-VEC commercial testing tool has also been performed. The techniques have been demonstrated to Crew Exploration Vehicle (CEV) clients from Johnson Space Center.

Presentations [PDF, 48K]

Practical Web Application Verification. April 2008.

Peter Mehlitz
Fujitsu Laboratories Ltd. and Fujitsu Laboratories of America, Inc. have developed the world’s first core technology for automatic verification of Java-based practical-use web applications. The verification system can automatically verify if a web application can operate properly to process specified task transactions without the need for manually preparing detailed test procedures or test data. It is based on Java PathFinder (JPF), the open source verification tool developed by NASA Ames Research Center. The JPF team of the Robust Software Engineering (RSE) group recently conducted a comprehensive field test with Fujitsu Laboratories of America and Fujitsu Japan to validate and maturate the JPF tool suite in the context of large industrial applications. Fujitsu Laboratories plans to conduct testing for an actual project, and will continue with research targeting practical use of this technology.

Presentations [PDF, 63K]

Pathfinder included in Google Summer of Code. March 2008.

Joe Coughlan
Java PathFinder (JPF) has been included in the 2008 Google Summer of Code (GSoC). Under this program, Google offers student developers stipends to write code for various open source projects. Over the past three years, GSoC has brought together over 1500 students and 2000 mentors from 90 countries worldwide. The PathFinder team will define the set of tasks the Google funding would support.

Presentations [PDF, 52K]

Small Spacecraft Team Prototype Vehicle Flight Tests. February 2008.

Karen Gundy-Burlet
The Small Spacecraft Common Bus team recently completed a series of successful prototype vehicle flight tests. The vehicle utilized a cold gas propulsion system to fly untethered for approximately five seconds. During this time, the vehicle demonstrated that it was able to maintain control of both position and orientation. To do this the team utilized an infrastructure and processes they have been developing for the generation of flight software for small spacecraft missions. The basis of these processes is to employ automatic software generation from system dynamics modeling tools such as Mathworks Simulink. Successful completion of this milestone demonstrates the team’s ability to utilize this technique for generating flight software. Roughly 85% of the flight software was automatically generated.

Presentations [PDF, 451K]

Joint Java Pathfinder Field Test With Fujitsu. July 2007.

Peter Mehlitz
The Java Pathfinder model checking tool architected and developed at NASA Ames Research laboratories was used to detect bugs in an internal Fujitsu code base that ran into one million lines of Java code. First the application was converted into a fully executable stand-alone Java model. With the active support of the NASA Ames team, the researchers at Fujitsu Laboratories of America (Sunnyvale) and Fujitsu Laboratories Limited (Kawasaki, Japan) were able to uncover injected (seeded) bugs in the application model that sent the model into panic mode. In this process the Java Pathfinder tool explored approximately 125,000 program states and millions of paths which would be impossible to cover using conventional testing techniques. The tool also uncovered an unexpected deadlock situation in the application model.

Presentations [PDF, 42K]

"Program Model Checking Practitioner's Guide" delivered to Software Assurance Research Program. April 2007.

Tom Pressburger
The final product of a three-year research initiative, a guidebook called "Program Model Checking: A Practitioner's Guide", was delivered to the Office of Safety and Mission Assurance's Software Assurance Research Program on April 27. This guidebook is directed at software developers and test engineers, and provides an introduction to program model checking technology and the methods and issues in applying it. The examples discussed in the guidebook are primarily NASA mission-critical and safety-critical software applications. The guidebook is available from a SARP website, search for "program model checking".

Presentations [PDF, 44K]

Analyzing Software Contribution to System Failures. December 2006.

Julian Richardson
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.

Presentations [Powerpoint, 120K]

Techniques For Compositional And Symbolic Analysis of Software. April 2006.

Corina Pasareanu, Dimitra Giannakopoulou, Willem Visser
Two key techniques in achieving scalability in the verification of large software systems are compositional and symbolic reasoning. Two papers describing work on compositional and symbolic reasoning for software verification were presented at the 13th International SPIN Workshop on Model Checking of Software. One describes automated compositional verification applied to a design model of the MER arbiter (a flight software module from JPL's Mars Exploration Rovers). The other describes novel approximate algorithms for performing state comparison during symbolic analysis of code. These algorithms enable pruning large portions of the explored program state space, therefore enabling more efficient verification.

Presentations [PDF, 50K]

Infusion of Software Engineering Research. March 2006.

Tom Pressburger, Lawrence Markosian
The software engineering technology infusion pilot projects that the Research Infusion subgroup of the intercenter Software Working group helped start have yielded benefits to NASA software development projects. Example benefits were detection of software defects that occurred in legacy code, or had escaped previous inspections and testing. Also, the development projects gave useful feedback to the technology developers and NASA about deployment concerns. Some of the technologies that were piloted have been adopted for future use by the projects. Technology transfer is a difficult task, and the subgroup seems to have found an inexpensive approach to introducing certain kinds of technologies.

Presentations [PDF, 237K]

Compositional Verification. August 2005.

Dimitra Giannakopoulou
Compositional verification achieved 100x savings in memory and 10x savings in time to complete the verification of the MER arbiter (a flight software module from JPL's Mars Exploration Rovers) in the SPIN model checker, as compared to exhaustive verification through model checking with non-compositional algorithms.A key step in achieving scalability in the verification of large software systems is to "divide and conquer"; that is, to break up the verification of a system into smaller tasks that involve the verification of its components.Over the last few years, the RSE group has developed a collection of techniques and a supporting toolset for performing assume-guarantee reasoning of software in an automated fashion.

Presentations [ PDF, 47K]

Efficient Software Verification Method Developed at Ames. July 2005.

Corina Pasareanu, Willem Visser
We have developed a new software verification method for efficient error detection. The method is automatic and reports counterexamples exhibiting errors, it can scale to the analysis of large systems and it is precise, meaning it does not report false positives. The novelty of the method is the integration of an abstract analysis with concrete program execution, and the use of a theorem prover to detect incompleteness of abstract analysis and to iteratively refine the analysis. The method has been applied successfully for error detection in RAX (Remote Agent Experiment) - a component extracted from a NASA embedded spacecraft control application, which deadlocked in space.In the future, we plan to apply the method to the analysis of other NASA mission software.

Presentations [ PDF, 355K]

Adaptable Program Synthesis. May 2005.

Julian Richardson
AutoFilter is a program synthesis system developed in the Robust Software Engineering group at NASA Ames. AutoFilter generates Kalman filter code from specifications of state estimation problems. Domain-specific program synthesis, e.g. as implemented in AutoBayes (data analysis) and AutoFilter can generate high quality code to solve problems in complex domains from clear, modular specifications. Commercial program synthesizers/generators typically yield 3-5x reductions in development time, 2x reductions in errors, and reduced maintenance costs. We have extended the AutoFilter synthesis system to allow users to specify application-specific code which is interleaved with the domain-specific synthesized code. Synthesis is automatic. This significantly extends the scope of the synthesis system This accomplishment significantly expands the scope of automatic synthesis, potentially extending its benefits to greater portions of NASA mission applications.

Presentations [ PDF, 210K]

Java Pathfinder Code Distributed Open Source. April 2005.

John Penix
JavaPathfinder (JPF) is part of an effort to develop tools and methods to identify and eliminate software errors in NASA's increasingly complex and mission-critical software systems. While specific research projects are focused on the verification and validation of NASA software, the recent open source distribution of JPF code enables the broader use and development of JPF capability for other NASA mission uses, and leverages the enthusiasm of the large number of developers in industry who are also working in this area.

Presentations [ PDF, 46K]

System Level Verification for Autonomy Software: Analysis of the K9 Rover Executive. August 2004.

Corina Pasareanu, Dimitra Giannakopoulou
Verification is essential for autonomy insertion into missions. Software errors are very expensive; traditional testing is hard for autonomous system due to high complexity and unpredictable environments. The benefits of our project is the development of scalable verification techniques applied early in the software life cycle, when it is cheaper to detect and fix bugs. Compositional techniques that automatically decompose global requirements into local properties, which are cheaper - in terms of time and consumed memory - to check. Increased level of confidence in reliability. Early detection of costly integration problems.

Presentations [ PDF, 433K]

Infusion of Software Engineering Research. July 2005.

Tom Pressburger, Lawrence Markosian
The goal of the NASA Software Engineering Initiative is to improve NASA software engineering to meet the challenges of NASA. One of the Initiative's objectives is to infuse software engineering research results into NASA practice. The Research Infusion subgroup of the intercenter Software Working Group has focused on getting NASA-sponsored software engineering research and leading edge commercial tools used on NASA projects. The approach is to select research, publicize it across NASA in a ViTS (a video teleconference presentation), and initiate pilot projects that deploy the research on NASA software development projects.

Presentations [ PDF, 250K ]

Automating the Documentation and Certification of NASA Software. May 2004.

Ewen Denney
The ASE group is developing automated program synthesis systems for the application domains of data analysis (AutoBayes) and state estimation (AutoFilter). We have previously extended these systems with an automated certification capability, based on mathematical logic, for various safety policies. However, it is very difficult for humans to interpret the resulting proofs and then relate them to the original program. We have addressed this by incorporating a safety documentation feature: a tool that can automatically generate textual explanations of safety with respect to a given safety policy for auto-generated code. This technology has the potential to increase confidence in the use of code generators within and outside NASA. Auto-generated code, in addition to a certificate of correctness (w.r.t. user-defined notions of safety) will come with a document containing human-readable explanation as to why it is correct. This approach is a significant step in the direction of merging formal certification with traditional certification.

Presentations [( PDF, 176K ),( Postscript, 640K ), ( PowerPoint, 253K )]

Simulation-Based Verification of Autonomous Controllers via Livingstone Path Finder. May 2004.

Charles Pecheur and Tony Lindsey
Model-based autonomous systems pose hard verification challenges because of the huge space of unpredictable circumstances in which they are expected to operate. Livingstone 2 (L2) is a model-based diagnosis system developed at NASA Ames, intended for autonomy applications. We developed Livingstone Pathfinder (LPF), an advanced verification tool for Livingstone 2. LPF features a scripting language for specifying, in a flexible and concise way, a large set of execution scenarios to be analyzed. The search engine explores the tree of possible executions according to different strategies, searching for discrepancies between actual and diagnosed state. We have successfully applied that technology on a real-size model (X-34 propulsion feed subsystem, 800+ variables, bottom two pictures). This case study demonstrated the scalability of the approach to large applications, and also detected an error that lead to a minor adjustment of the X-34 model.

Presentations [( PDF, 821K ),( Postscript, 1.4M ),( Powerpoint, 431K )]

Verification of Diagnosability using Model Checking. April 2004.

Charles Pecheur
A diagnosis system locates the faults in a physical system (such as a spacecraft) based on observations from sensors and actuators. An important characteristic of a physical system is its diagnosability; i.e., whether there are sufficient observables to pinpoint faults. Our work involves a novel approach to verifying that a system can be properly diagnosed. We use a model of the system and advanced symbolic model-checking techniques that allow the exhaustive analysis of all possible executions of that system, even for very large state spaces. We have successfully demonstrated that technology on a real-size model, an X-34 propulsion feed subsytem.

Presentations [( PDF, 330K ),( Postscript, 778K ),( Powerpoint, 192K )]

Lightweight Automatic Generation of Traceability Information. December 2003.

Julian Richardson
Tracing from a program's requirements to the parts of the program which implement those requirements is important- by linking related artifacts in a software development, it can help to ensure that consistency is maintained as the software evolves, and help to pinpoint software errors. Traceability is required by the avionics standard DO-178B. Programmers input traceability information manually into tools such as DOORS. This information is hard to derive, requiring understanding of both problem domain and program, and hard to maintain when the program or requirements change. Synthesis systems and compilers can be extended to derive traceability information in parallel with the synthesis/compilation process, but this has previously required extensive modification of the entire synthesis system. We have developed a new, very lightweight technique for deriving traceability information which works with any kind of automatic generation process.

Presentations [( PDF, 116K ),( Postscript, 327K ),( Powerpoint, 145K )]

Software Engineering Research Infusion ViTS. November 2003.

Thomas Pressburger and Lawrence Markosian
The Research Infusion subgroup of the intercenter Software Working Group is being led by Tom Pressburger and has focused on bringing NASA-sponsored software engineering research and leading edge commercial tools to the attention of NASA software developers. On Sept. 23, Lawrence Markosian and Tom Pressburger gave an hour long ViTS (video presentation) to an audience of 115 civil servants and contractors, including engineers, leads, managers, and quality assurance personnel, across 11 NASA centers. Markosian presented overviews of seven software engineering technologies with the goal of starting collaborations between NASA software developers and researchers.

Presentations [( PDF, 220K ),( Postscript, 625K ),( Powerpoint, 996K )]

Confidence Tool for Neuro-Adaptive Controllers. September 2003.

Johann Schumann and Pramod Gupta
Software for safety-critical tasks (e.g., aircraft control) must undergo rigorous verification and validation (V and V) before it can be deployed. The primary motivation of this work is to enable the use of neural networks (NN) in safety-critical control applications. The aerospace industry has perceived neural networks as inherently unpredictable, and therefore difficult to certify. The goal of the work is to develop techniques and tools for rigorous V&V of NN based adaptive controllers ultimately supporting their certification, major prerequisite for most NASA applications. Our approach combines mathematical analysis with dynamic monitoring to ensure robust convergence and stability. We have implemented a prototypical tool, using a Bayesian approach to analyze the (Gaussian) probability distribution of the neural network output which describes the quality of the NN performance. Our confidence tool can be used for pre-deployment verification, and, as a prototype software harness to monitor quality of adaptation during the mission.

Presentations [( PDF, 314K ),( Postscript, 782K ),( Powerpoint, 633K )]

Extending Code Generators with Certification Capability. July 2003.

Ewen Denney
The ASE group is developing synthesis systems which are able to automatically generate a wide range of complex programs in the NASA-relevant domains of date analysis and state estimation. We have extended these systems with the capability of generating annotated code which can then be automatically verified for compliance with a given safety property. The main increment over previous work is in extending the program synthesis system so that it is customizable with respect to different notions of safety. The certification is significantly more accurate (fewer false positives)than commercial analysis tools. This technology has the potential to increase confidence in the use of code generators within and outside NASA.

Presentations [( PDF, 182K ),( Postscript, 567K ),( Powerpoint, 156K )]

Correctness of Software Safety Policies. April 2003.

Ewen Denney
Program certification techniques formally show that programs statisfy certain safety policies. They rely on the correctness of the safety policy which has to be established externally. We have developed a framework which is generic with respect to safety policies and which allows us to establish that proving the safety of a program statically guarantees dynamic safety, i.e. that the program never violates the safety property during its execution. We have formalized a selection of safety properties in our framework, and shown that they are sound and complete with respect to a semantic notion of safety. We have developed a generic method of doing this for arbitrary safety properties, thus showing how a safety policy can be automatically derived from a safety property and an operational semantics. Safety assurance is a necessary precondition for the application of code generation technology in safety-critical areas.

Presentations [( PDF, 169K ),( Postscript, 514K ),( Powerpoint, 171K )]

Automatic Software Design Document Generation. March 2003.

Bernd Fischer, Phil Oh, and Johann Schumann.
Autocoding techniques promise large gains in software development productivity. Program synthesis systems can generate large C++ programs that sovle NASA-relevant problems, such as those used in guidance applications. However, the real-world application of autocoding technology has been limited, particularly in areas where a rigorous software development process is used. Because the automatically generated code needs to be tested, integrated, and certified, synthesis of code alone is not sufficient: the generated code must be readable and understandable. For practical usability, we have extended our generator of Software Design Documents (SDD). This technology has the potential to substantially increase the use of autocoding technology within NASA, as the generated standarized and detailed design document facilitatess integration of the synthesized code into a rigorous software development process including code review, testing, and certification.

Presentations [( PDF, 191K ),( Postscript, 618K ),( Power Point, 536K )]

V and V of Neural Networks. March 2003.

Pramod Gupta and Johann Schumann
The main goal of this research is to develop methods and techniques that allow for rigorous verification and validation of neural-network based controllers. For safety-critical applications, a neural-network based controller must be verified and validated thoroughly and must pass a rigorous certification procedure; something yet to be accomplished. When neural networks are used in prediction problems, it is usually desirable that some form of confidence bound is placed on the predicted value. The bound gives the range of the output of the neural network within which performance of the neural network is good satisfactory. Our approach analyzes the probability distribution of the neural network output.

Presentations [( PDF, 223K ),( Postscript, 574K ,( Powerpoint, 946K )]

NN Process Guides-Increases Safety and Reduce Cost. March 2003.

Stacy Nelson
The goal of this project is to document how to develop neural networks in adaptive Intelligent Flight Control Systems (IFCS) in accordance with NASA and FAA safety/mission-critical certification standards. Adaptive IFCS makes it possible for a pilot to land a damaged aircraft that might otherwise crash. Testing these highly advanced flight control systems is very difficult. To date, processes and methods have been proven and documented for pre-trained neural networks (PTNN). Work is underway to document processes and methods for Real-Time Adaptive NN (RANN). RANN are trained druing flight and provive better adaptive capabilities but are more difficult to verify and validate.

Presentations[( PDF, 246K ),( Postscript, 712K ),( Powerpoint, 920K )]

Component Assumptions. February 2003.

Presentations[( PDF, 128K ),( Postscript, 426K ),( Powerpoint, 156K )]

Presentation on System-Level Verification for Autonomous Systems: Automatic Assumption Generation for Component Verification. February 2003.

Dimitra Giannakopoulou and Corina Pasareanu
Assume-guarantee reasoning is a divide and conquer approach to verification of large systems that makes use of "assumptions," i.e., abstractions of the environment of a system component. Although aimed at scalablility, such reasoning has not been widely applied, because coming up with appropriate assumptions is a difficult manual process. We have developed a novel framework for incremental, and fully automated assume-guarantee reasoning. We have extended our approach from safety violations to deadlock. It has been successfully applied to the executive of the DS-1 Remote Agent.

Presentations [( PDF, 249K ),( Postscript, 655K ),( Powerpoint, 286K )]

High Level Data Race Detection. February 2003.

Klaus Havelund
High-level data races occur when different activities, that execute in parallel, access shared resources, but with different atomicity views. This may cause such activities to obtain inconsistent snapshots of the shared resources. A high-level data race was for example present in the Deep Space 1 Remote Agent. We have developed a runtime analysis algorithm for high-level data race detection, and have applied the algorithm to several case studies, including the Ames K9 Rover.

Presentations [( PDF, 187K ),( Postscript, 603K ), ( Powerpoint, 221K )]

Certification Support for Automatically Generated Programs. January 2003.

Johann Schumann
Auto-generated code has many advantages; e.g., it requires less effort to produce, and its specification is more maintainable. But autocoding technology comes with risk: how can the correctness of the generated code be assured? Our solution is not to try to verify the code-generator; rather, we automatically verify safety properties (e.g., array-bound safety, variable initialization safety) for each generated piece of code. We extended the AutoBayes program synthesis system (which generates data analysis programs, e.g., for clustering and time-series analysis) to automatically generate annotations for the selected properties. With a Verification Condition generator, we then produced logical conditions which were then automatically proven using an automated theorem prover. This technology has the potential to increase confidence in the use of code generators within and outside NASA.

Presentations [( PDF, 169K ),( Postscript, 535K ),( Powerpoint, 154K )]

Runtime Verification with Java PathExplorer. December 2002.

Klaus Havelund
The Java PathExplorer tool provides a set of algorithms for instrumenting and monitoring Java programs. A program is instrumented to emit events when executed. The event stream makes up an execution trace, which is then analyzed by the different algorithms. The tool has new, efficient algorithms for detecting deadlocks and data races, and violations of temporal logic formulas.

Presentations [( PDF, 213K ),( Postscript, 682K ),( Powerpoint, 250K )]

ASE Group Program V&V History 1997-2002. December 2002.

Klaus Havelund and Willem Visser
Havelund and Visser were invited as special guest editors for a special Ocotber 2002 issue of the STTT journal (International Journal on Software Tools for Technology Transfer) containing a selection of best papers from the conference. As part of this job they wrote a guest editor article, "Program Model Checking as a New Trend" that gives their views and experiences in the field of software model checking. Havelund and Visser are generally considered to be pioneers in this field. Two versions of the Java PathFinder tool that model check Java programs, and that have been developed in the ASE group by the POCs, have considerably influenced the international research community in this new field.

Presentations [( PDF, 205K ),( Postscript,600K ), ( Powerpoint, 394K )]

Using Model Checking to Discover Automation Surprises. November 2002.

Guillaume Brat and Willem Visser
Using model checking to discover automation surprises. The aim of this work is to develop an automated approach to identify mode confusion problems in automation used in modern aircraft and spacecraft. These problems arise when a pilot thinks a plane is one mode when the plane is actually in another mode. Previous work in this area required to model the machine (flight control system), the user (pilot), its task, and the interface (cockpit display) in a formal language. In our work, all can be done using the actual code that is flown. Hence, we achieve a substantial gain in terms of fidelity of analysis. We also simplify and automate the task of verifying these interactive systems.

Presentations [( PDF, 177K ),( Postscript, 626K ), ( Powerpoint, 217K )]

V and V of Neural Networks. November 2002.

Pramod Gupta and Johann Schumann
Artificial neural networks (ANN) offer a powerful and versatile computational model for adaptive controllers. A major benefit of such a controller is a n ability to adapt to unforeseen events, e.g., loss of an actuator. ANN based adaptive controllers will be of high importance to ensure mission success. The goal of this work is to develop methods and techniques that allow for rigorous V and V of ANN based adaptive controllers ultimately supporting their certifacation - a major prerequisite for most NASA applications. We are designing and implementing a prototype software harness that monitors quality of adaptation during the mission, by computation of confidence intervals.

Presentations [( PDF, 272K ),( Postscript, 743K ),( Powerpoint, 609K )]

Explaining the Cause of an Error. November 2002.

Willem Visser
In previous work we have shown that a model checker can be used to autmatically find transient errors, such as those caused by concurrency related problems. However, a model checker only produces an error trace and does not give any guidance of what the cause of the error is; here we address this second problem by introducing a technique whereby the cause of an error is explained. The error explanation algorithm have been implemented in the Java PathFinder model checker toolset. It has been used to explain errors in a number of complex software systems, including the DEOS real-time operating system and the Mars K9 Executive prototype.

Presentations [( PDF, 177K ),( Postscript, 569K ),( Powerpoint, 211K )]

Certification Technology for Auto-generated Code. November 2002.

Jonathan Whittle
Autofilter is a code generator geared towards state estimation problems (e.g., attitude estimation, parameter estimation). We have designed an extension to Autofilter so that in addition to the code it generates a proof that the algorithm inherent in the code is statistically optimal. This technology has the potential to increase the confidence in the use of code generators within and outside NASA.

Presentations [( PDF, 191K ),( Postscript, 802K ),( Powerpoint, 290K )]

Generating Assumptions. November 2002.

Dimitra Giannakopoulou and Corina Pasareanu
Assume-guarantee reasoning is a divide and conquer approach to verification of large systems that makes use of "assumptions," i.e., abstractions of the environment of a system component. Although aimed at scalability, such reasoning has not been widely applied, because coming up with appropriate assumptions is a difficult manual process. We have developed a novel framework for incremental, and fully automated assume-guarantee reasoning. It has been successfully applied to a number of case studies, including the Mars K9 Executive prototype.

Presentations [( PDF, 118K ),( Postscript, 469K ),( Powerpoint, 157K )]

Generalized Symbolic Execution for Model Checking and Testing. November 2002.

Corina Pasareanu and Willem Visser
A novel symbolic execution framework was developed and an algorithm implemented that enables model checking of programs that have complex inputs with unbounded (very large) data. The symbolic execution algorithm has been implemented in the Java PathFinder model checker toolset. It has been used to generate test inputs for code coverage (i.e., condition coverage) of an Altitude Switch used in flight control software.

Presentations [( PDF, 180K ), ( Postscript, 572K ),( Powerpoint, 173K )]

Deadlock Analysis with Fewer False Positives. November 2002.

Klaus Havelund
Concurrency-related errors in multi-thread ed mission software often manifest themselves only by intermittent bugs and hence are difficult to find by testing. Runtime Analysis is a solution; it is a technique that analyzes the trace of a single execution of a program, inferring possible problems in other executions. It scales well to large programs. We have developed an enhanced runtime analysis algorithm for deadlock detection that issues fewer false positives than the standard algorithm. This algorithm, and a data race detection algorithm, have been implemented in the Java PathExplorer (JPax) runtime verification tool. JPax has been applied to two major case studies, the K9 rover developed at Ames and the Deep-Space 1 attitude control system.

Presentations [( PDF, 548K ),( Postscript, 1.1M ),( Powerpoint, 266K )]

Verification for Next-Generation Space Shuttle. November 2002.

Charles Pecheur
A survey was published that was performed at NASA Ames in support of developing V and V methods within the IVHM (integrated vehicle health management) architecture development project led by Northrop Grumman Corp.(NGC) for the Next-Generation Space Shuttle. It is part of an overall project on V and V of model-based reasoning.

Presentations [( PDF, 155K ),( Postscript, 671K ),( Powerpoint, 113K )]

Back to Top

Last modified: Feb. 05, 2007 by Hamed Jafari.