Automated Software Engineering Technologies (ASET)
Project Manager: Michael Lowry, Ph.D., NASA Ames Research Center
The goal of the ASET project is to develop automated tool support for a mathematically based discipline of software engineering. NASA's reliability and confidence in its software systems for mission and safety critical applications have been identified as a high priority. ASET is developing technologies and tools to significantly enhance the safety of digital aeronautical systems and the productivity of engineers who develop these systems. ASET research includes formal methods for requirements and design specification, automated code generation, and high-assurance design techniques. It also includes appropriate verification and validation methods for these new technologies. ASET aims for a total systems approach to these objectives.
ASET's principal government customers are the Space Science Enterprise (Code S) and the Aerospace Technology Enterprise (Code R). Its principal industry customers are Honeywell and SRI International.
ASET's three main research elements are:
Program Synthesis
Program synthesis through automated logical reasoning has the potential to address reliability, cost, and scheduling. This element is investigating efficient algorithms for automated high-assurance generation of software designs and code from requirements and specifications. The objective is to scale up new code-generation methods being developed in the research community that are intrinsically high-assurance, but not yet computationally efficient. A secondary objective is to develop technology for safely and efficiently reusing software (including design, architecture, and code), thus leading to avionics product families.
High-Assurance Software Design
This element is investigating and developing tools to increase the integrity and reliability of software for safety-critical and mission-critical flight applications. The emphasis is on scaling up and automating analytical methods for verification and debugging across the software life cycle. This effort extends the application of formal methods into later areas of the software development life cycle to include design and implementation.
Formal Methods for Requirements
This element is investigating the use of mathematical specification and verification of software requirements and design as a means of increasing the reliability of digital avionics systems. This element focuses on the requirements/design stages of aerospace software development. This is a departure from the more traditional software development methodologies, which rely on careful process management of the software development life cycle to provide reliability. While the main focus is on the application of verification theorem proving to aerospace requirements/design, this element also identifies gaps in the underlying theorem-proving technology and funds needed improvements in the technology.
ASET Project Milestones
High Assurance Program Synthesis: Development of technologies to enable the semi-automated synthesis of provably correct programs from a high-level specification in a manner that allows domain experts to customize and extend the tools.
- Development of automated certification algorithms that take code with annotations and prove adherence to properties. (Project milestone 8.2.1)
- Demonstration of a program synthesis engine that generates both code and annotations for certification via logic-based analysis. (Project milestone 8.2.2)
- Demonstration of algorithms that take knowledge representations from domain experts and transform them to program-synthesis capabilities. (Project milestone 8.9.1)
- Demonstration of methods and tools enabling domain experts to debug extensions they make to program synthesis system. (Project milestone 8.9.2)
Analytical Verification and Debugging: Development of technologies used to formally analyze code to detect, isolate and recover from software errors during the development of the software and at run-time.
- Development of V&V techniques that minimize run-time monitoring. (Project milestone 8.8.1)
- Development of methods for recovery from run-time errors using sophisticated monitoring. (Project milestone 8.8.2)
Formal Methods for Requirements: Development of techniques for formal specification of requirements to enable a formal process for software verification and validation.
Top
