Specification Editing and Discovery Assistant

Award Information
Agency:
National Aeronautics and Space Administration
Branch
n/a
Amount:
$125,000.00
Award Year:
2013
Program:
SBIR
Phase:
Phase I
Contract:
NNX13CL55P
Award Id:
n/a
Agency Tracking Number:
124308
Solicitation Year:
2012
Solicitation Topic Code:
A1.06
Solicitation Number:
n/a
Small Business Information
NY, Ithaca, NY, 14850-3250
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
603978321
Principal Investigator:
David Cok
Assoc. VP of Technology
(607) 273-7340
dcok@grammatech.com
Business Contact:
Derek Burrows
General Counsel
(607) 273-7340
dburrows@grammatech.com
Research Institute:
Stub




Abstract
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.

* information listed above is at the time of submission.

Agency Micro-sites


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government