Small Business Innovation Research/Small Business Tech Transfer
Specification Editing and Discovery Assistant, Phase I
Project Description
The project will prototype a specification editing and discovery tool (SPEEDY) for C/C++ that will assist software developers with modular formal verification tasks by - providing active user interface guidance in writing and editing software specifications, integrated into a common, open IDE (Eclipse) and - providing automated suggestions of specifications for given contexts, - built on an architecture that will unify source and machine code verification. The innovation is significant because - having machine-checkable specifications enables more automation of sound verification and less approximation in heuristic problem detection, - user interface features and underlying automation will aid all developers in generating, editing and checking specifications, and - the architecture will apply to both source code analysis alone and also to unified source and machine code verification for embedded systems. The prototype will be an extension and integration of (a) current specification languages, (b) previous Eclipse plug-ins GrammaTech has created, (c) recent research on UI aids to developers in writing specifications, (d) existing automated algorithms for suggesting specifications based on code analysis, and (e) existing tools and techniques for automatically checking logical encodings of C/C++ code and specifications. The tool will be packaged as a plug-in to Eclipse's C/C++ development environment. The result will be a tool that facilitates using formal methods by all software developers, improving efficiency and accuracy. The resulting specifications will also serve as machine-readable documentation of the software, simplifying and accelerating the task of independent V&V.
More »
Anticipated Benefits
The product will be used to assist NASA personnel in evaluating the safety and robustness properties of software in production or under review, including embedded Next-Generation avionics and space software. The product will support the needs of both software-development teams and IV&V groups. An example application is the annotation of a widely used library (e.g. the Core Flight Software library) to aid in its verification. Our first potential (NASA) adopters are GrammaTech's current NASA customers. The tool will be a natural companion to heuristic bug-finding and style-checking tools GrammaTech completed for NASA JPL (a JPL SBIR Success Story used for the Mars Science Laboratory software. The natural market for SPEEDY is safety-critical embedded software development organizations. Such government and commercial organizations are a large part of GrammaTech's current customer base. We will initially focus our marketing efforts on specific current customers who manufacture or review avionics systems, medical devices, and other particularly safety-critical embedded systems (e.g. automotive software) – e.g., Bechtel, FDA, Halliburton, Lockheed-Martin, Honeywell. A second tier of relevant customers are development groups doing security analyses, security certification, and reverse engineering for understanding or maintenance.
More »
Project Library
Primary U.S. Work Locations and Key Partners
| Organizations Performing Work | Role | Type | Location |
|---|---|---|---|
| GrammaTech, Inc. | Lead Organization | Industry | Ithaca, New York |
Langley Research Center
(LaRC)
|
Supporting Organization | NASA Center | Hampton, Virginia |
Primary U.S. Work Locations
-
New York
-
Virginia
Suggest an Edit
Recommend changes and additions to this project record.