Suggested Searches

Robust Software Engineering

Overview

We are the Robust Software Engineering technical area, based in the Intelligent Systems Division at NASA’s Ames Research Center at Moffett Field, California.

Our goal is to dramatically increase the reliability and robustness of NASA’s mission related software, and the productivity of its software engineering, through the research, development, application, and transfer of automated software engineering technology that scales to meet NASA’s software challenges. We draw upon many techniques from Computer Science (for example, in the areas of program verification, automated reasoning, model checking, static analysis, symbolic evaluation, and machine learning) and apply them to the verification and validation of software, as well as code generation. Technologies we developed include automated software analysis, automated test case generation, reliable code generation, and risk prediction and analysis.

We applied our technologies to NASA projects involved with Space and Aeronautics, and spun off sample educational lessons for students and teachers. We are currently engaged with projects in all the NASA Mission Directorates: Human Exploration & Operations, Aeronautics, and Science.

Our Core Avionics & Software Technologies (CAST) group also develops flight software for small spacecraft missions.

Research Themes

Verification and Validation
The objective of this project is to apply and develop analytic verification technology. Analytic tools rely on algorithms that mathematically analyze specifications, code, and models for consistency with requirements and designs. This provides a complementary and higher level of debugging and V&V than traditional testing methods alone.

Synthesis Projects & Applications (not currently active)
Program synthesis is the systematic, usually automatic, construction of correct and efficient executable code from declarative specifications. We are developing this technology primarily for application in the domains of data analysis and state estimation. We are also interested in correctness issues, specifically regarding the formal certification of synthesized code.

Projects

  • Advanced Testing explores ways of making testing more efficient, expanding its coverage, or making testing find subtle problems often corresponding to boundary cases, and include tools such as Symbolic Execution, MARGInS, and Adaptive Stress Testing (AdaStress).
  • Code Analysis includes formal techniques to analyze code and different programming languages, and it includes tools such as Inference Kernel for Open Static Analyzers (IKOS), or Java PathFinder (JPF).
  • Code Synthesis is about formally automatically generating code, sometimes for specific domains, and it includes tools such as AutoBayes (Synthesis of Data Analysis Software) or Certifiable Synthesis.
  • Design Model is a project that focuses on various techniques to enable V&V at early development stages, and it includes tools and techniques such as Compositional Verification, Java PathFinder (JPF), and CoCoSim.
  • Requirement Analysis is about the elicitation of requirements that are as close to plain English as possible but are formalizable, and thus analyzable and amenable to be used as formal properties in analysis, as shown in the Formal Requirements Elicitation Tool (FRET).
  • Safety Assurance is investigating alternative paths to certification (especially in aviation) and building tools to support it, which is shown in the Assurance Case Automation Toolset (AdvoCATE) for safety cases.
  • Autonomy and Artificial Intelligence is a new, and very important target for our V&V and assurance work, and it includes topics such as Verification and Validation of Adaptive Control Software, AdaStress, and Safe Deep Neural Networkds (SafeDNN).
  • Runtime Monitoring and Analysis is a complementary project, which investigates various forms of runtime analysis and monitoring for both on-board solutions and ground support, and it includes technology such as Runtime for Airspace Concept Evaluation (RACE) to support fusion and analysis of concurrent, live and/or simulation, data streams so that tools like Message-based Systems Analysis (MESA) or Realizable Responsive UnobtrusiveUnit (R2U2, Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systetems) can be used.

Technical Area Lead
Guillaume P. Brat

Deputy Area Lead
Sandy Lozito

Group Members

Caleb Adams
Adrian Agogino
Sequoia Andrade
Mari Aoki
Wyatt Cannon
Corey Carter
Divya Gopinath
Guillaume Brat
Misty Davies
Ewen Denney
Orlando Diaz
Yuning He
Daniel Hulse
Lukman Irshad
Stephen Jacklin
Andreas Katis
Matthew Knudson
Caroline Lassiter
Robert Lim
Rory Lipkis
Ignacio Lopez-Francos
Anastasia Mavridoiu
Seydou Mbaye
Peter Mehlitz
Jonathan Menzies
Sarah Mitchell
Ganesh Pai
Corina Pasareanu
Ivan Perez
Thomas Pressburger
Johan Schumann
Nija Shi
Irfan Sljivo
Walter Vaughan
Pavlo Vlastos
Hannah Walsh
Aaron Woodard

RSE Point of Contact
Guillaume P. Brat
Technical Area Lead

RSE Affiliates
Joseph C. Coughlan
Former Technical Area Lead, 2009-15

Dr. Michael Lowry
Chief Scientist

CAST Members
Nathan Benz
Joseph Castle
Scott Christ
Howard Cannon
Edmund De la Cruz
Vinh Doan
Kandy Fabreo
Leigh Garbs
Mohammad Hejase
Michael Ho
Tony Koudsi
Robert Lim
Matthew Knudson
Andrew Mikhail
Craig Pires
John Rasmussen
James Roach
Todd Sarshad
Kevin Seywald
Dave Varvell