NASA SBIR 2010 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER: 10-1 A1.14-8778
SUBTOPIC TITLE: Verification and Validation of Flight-Critical Systems
PROPOSAL TITLE: Continuous Integrated Invariant Inference

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
GrammaTech, Inc.
315-317 N. Aurora Street
Ithaca, NY 14850 - 4201
(607) 273-7340

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
David R Cok
dcok@grammatech.com
317 N. Aurora St.
Ithaca, NY 14850 - 4201
(607) 273-7340 Extension :46

Estimated Technology Readiness Level (TRL) at beginning and end of contract:
Begin: 3
End: 5

TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
The proposed project will develop a new technique for invariant inference and embed this and other current invariant inference and checking techniques in an easy-to-use tool. The result will enhance an engineer's ability to use formal methods – generating, editing, reviewing, proving and testing invariants – and improve productivity in verification and validation of safety and correctness properties software.

Currently, invariants that represent such properties require extensive human effort to write; automated techniques, though improving, are still insufficiently capable of automatically inferring them.

The proposed project will develop innovative techniques to infer logical invariants describing the behavior of individual software modules by combining static (analyzing a program without running it) and hybrid analysis (inferring invariants from observations of executing software). In particular, the project will (a) combine concolic execution and hybrid analysis to find candidate invariants from high-branch-coverage test suites, (b) apply that combination to obtain invariants for individual functions and data structures, (c) iterate the analysis to broaden data coverage of the test suite and improve the accuracy of invariants, and (d) create early prototypes and development plans to integrate the resulting tools in selected IDEs (Eclipse and GrammaTech's CodeSonar tool).

In carrying out this project, GrammaTech will build on its static analysis tools, concolic engine, and software dynamic translation module. It will leverage its base of research and expertise in static and hybrid analysis, specification languages, automated SMT theorem provers, and GUI tools for program analysis and development. The commercialization prospects for the proposed project are enhanced by GrammaTech's demonstrated experience in producing prototypes and commercial products from research results.

POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The project will target NASA activities concerned with verification and validation, safety-critical avionics (including the NextGen air traffic control system), and with assessment of COTS or third party software to be included in critical systems. GrammaTech will seek reviews and early adopters of the developed technology among the company's current customers of its existing products in several of NASA's facilities. For example, GrammaTech has worked closely with the LaRS group at JPL in developing other product enhancements and would solicit their review of this new technology; in addition, GrammaTech's static analysis tools are in current use in NASA's V&V facilities.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The project expects to market a commercial version of the tools it generates first to existing GrammaTech customers, particularly with early adopter releases. The most relevant application areas are safety-critical and correctness-critical software: software for medical devices, commercial avionics, automotive systems, and other embedded software. The capability to operate on machine code without source code will be useful for customers needing reverse engineering or security analysis tools. The tool's test generation capabilities will also be attractive to desktop software manufacturers that may not be interested in verification of software properties. GrammaTech will enlist some current customers as early adopters. Among its active customers are facilities whose task is software inspection and certification; the company expects that these will be natural reviewers and customers for the project's technology. The project anticipates that placing the new technology in existing IDEs will smooth the path to initial experimentation and eventual adoption of the new technology.

TECHNOLOGY TAXONOMY MAPPING (NASA's technology taxonomy has been developed by the SBIR-STTR program to disseminate awareness of proposed and awarded R/R&D in the agency. It is a listing of over 100 technologies, sorted into broad categories, of interest to NASA.)
Avionics (see also Control and Monitoring)
Development Environments
Programming Languages
Quality/Reliability
Simulation & Modeling
Software Tools (Analysis, Design)
Verification/Validation Tools


Form Generated on 09-03-10 12:12