{"project":{"acronym":"","projectId":17806,"title":"Specification Editing and Discovery Assistant","primaryTaxonomyNodes":[{"taxonomyNodeId":10643,"taxonomyRootId":8816,"parentNodeId":10640,"level":3,"code":"TX04.6.3","title":"Robot Software","definition":"Robot software provides architectures, frameworks, design patterns, and advances in software to enable the realization of intelligent robots from component technologies, and providing standardized interfaces and messages. Challenges include managing overall software complexity, striking the right balance between flexibility and complexity, and addressing heterogeneity of hardware.","exampleTechnologies":"Robotic architectures and frameworks, standardized messaging protocols, model-based robotic software, robot operating systems","hasChildren":false,"hasInteriorContent":true}],"startTrl":3,"currentTrl":6,"endTrl":6,"benefits":"We envision these use cases for SPEEDY's specification discovery and manipulation features: 1) Developers creating implementation and specifications together, with continuous automated checking 2) Developers writing code to specifications previously created by experts who have designed and verified core algorithms 3) Understanding and reverse engineering existing (legacy) code 4) Code Review of code under development 5) V&V teams inspecting developed code NASA has applications across these use cases. There are four particular categories of potential users. 1) NASA developers implementing safety-critical avionics or space-flight software can use SPEEDY in use cases 1, 2 and 4 above. SPEEDY helps them introduce formal methods into their work processes without having to swim (and sink) in the details of logics, provers, and verification conditions. 2) NASA formal methods teams have the task of verifying core designs and protocols. But once designed, the result must be communicated to developers and implemented correctly. Formal specifications provide a way to enable and check this communication, and SPEEDY provides a tool in which to accomplish it easily. This is use case #2. 3) NASA V&V teams can make ready use of use cases #4 and #5. 4) NASA developers faced with old code or changing team members will welcome the capabilities of use case #3.
Our target market for the eventual SPEEDY product is safety and security-critical software development engineers and organizations. We are building on the current trend toward more logical formality in software development. The bulk of that market develops embedded software; this is the same market space that is addressed by GrammaTech's existing products. We believe there is an early-adopter segment of that market that is willing to increase the level of model checking/software verification/formal reasoning during software development. But we are sure this need will be satisfied only if there are tools that provide the right capabilities, in the developers' working environment, targeted to non-formal-methods experts. This market growth will be particularly the case for embedded (and robotic) software, as such software will be increasingly important to an ever more technological society. We will initially focus our (non-NASA) marketing efforts on current customers who manufacture avionics systems, medical devices, and other safety-critical embedded systems (e.g. automotive software) – e.g., FDA, Covidien, Lockheed-Martin, and Honeywell. A second tier of relevant customers is development groups doing security analyses, security certification, and reverse engineering for understanding or maintenance.","description":"Accurate safety analysis of software suffers from a lack of appropriate tools for software developers. Current automated tools require approximate analyses; fully-assured verification with formal methods is expert-intensive. A key to improvement is machine-checkable specifications for software modules. Specifications are also needed to express the intent of software. Further, to scale to wide use, engineers who are not formal methods experts must have usable tools, as automated as possible, integrated into their usual software development environments (IDEs). Our proposal, SPEEDY, is a user experience (UX) design for convenient generation, manipulation, and checking of specifications, directly in a common IDE (Eclipse). The tool's design integrates automated specification suggestion using current tools and published techniques. The tool also enables checking and debugging specifications directly in the IDE, with information presented in the context of the source code. The proposal targets C/C++ programs, particularly for embedded software development. Phase I of SPEEDY assessed current specification languages and prototyped the key UX mechanisms: we are now confident that they can be implemented in the Eclipse IDE. We also integrated several analysis tools, demonstrating that SPEEDY can obtain specification suggestions from external sources. We assessed many specification suggestion algorithms, selecting some to be implemented and evaluated on realistic software in Phase II. Phase I also prototyped the integrating specification checking tools and specification debugging features. We demonstrated SPEEDY on NASA software from the NASA open software site. The Phase II proposal presents a plan for scaling up the successful Phase I prototype in many dimensions: more language features; more sophisticated user guidance in generating and debugging specifications; more specification suggestion algorithms; scaled up to realistic program size.","startYear":2014,"startMonth":4,"endYear":2016,"endMonth":4,"statusDescription":"Completed","principalInvestigators":[{"contactId":105052,"canUserEdit":false,"firstName":"David","lastName":"Cok","fullName":"David Cok","fullNameInverted":"Cok, David","primaryEmail":"dcok@grammatech.com","publicEmail":true,"nacontact":false}],"programDirectors":[{"contactId":206378,"canUserEdit":false,"firstName":"Jason","lastName":"Kessler","fullName":"Jason L Kessler","fullNameInverted":"Kessler, Jason L","middleInitial":"L","primaryEmail":"jason.l.kessler@nasa.gov","publicEmail":true,"nacontact":false}],"programExecutives":[{"contactId":215154,"canUserEdit":false,"firstName":"Jennifer","lastName":"Gustetic","fullName":"Jennifer L Gustetic","fullNameInverted":"Gustetic, Jennifer L","middleInitial":"L","primaryEmail":"jennifer.l.gustetic@nasa.gov","publicEmail":true,"nacontact":false}],"programManagers":[{"contactId":62051,"canUserEdit":false,"firstName":"Carlos","lastName":"Torrez","fullName":"Carlos Torrez","fullNameInverted":"Torrez, Carlos","primaryEmail":"carlos.torrez@nasa.gov","publicEmail":true,"nacontact":false}],"projectManagers":[{"contactId":280652,"canUserEdit":false,"firstName":"Kurt","lastName":"Woodham","fullName":"Kurt P Woodham","fullNameInverted":"Woodham, Kurt P","middleInitial":"P","primaryEmail":"kurt.woodham@nasa.gov","publicEmail":true,"nacontact":false},{"contactId":461333,"canUserEdit":false,"firstName":"Theresa","lastName":"Stanley","fullName":"Theresa M Stanley","fullNameInverted":"Stanley, Theresa M","middleInitial":"M","primaryEmail":"theresa.m.stanley@nasa.gov","publicEmail":true,"nacontact":false}],"website":"","libraryItems":[{"file":{"fileExtension":"pdf","fileId":292203,"fileName":"SBIR_2012_2_BC_A1.06-9692","fileSize":65814,"objectId":288718,"objectType":{"lkuCodeId":889,"code":"LIBRARY_ITEMS","description":"Library Items","lkuCodeTypeId":182,"lkuCodeType":{"codeType":"OBJECT_TYPE","description":"Object Type"}},"objectTypeId":889,"fileSizeString":"64.3 KB"},"files":[{"fileExtension":"pdf","fileId":292203,"fileName":"SBIR_2012_2_BC_A1.06-9692","fileSize":65814,"objectId":288718,"objectType":{"lkuCodeId":889,"code":"LIBRARY_ITEMS","description":"Library Items","lkuCodeTypeId":182,"lkuCodeType":{"codeType":"OBJECT_TYPE","description":"Object Type"}},"objectTypeId":889,"fileSizeString":"64.3 KB"}],"id":288718,"title":"Briefing Chart","description":"Specification Editing and Discovery Assistant, Phase II Briefing Chart","libraryItemTypeId":1222,"projectId":17806,"primary":false,"publishedDateString":"","contentType":{"lkuCodeId":1222,"code":"DOCUMENT","description":"Document","lkuCodeTypeId":341,"lkuCodeType":{"codeType":"LIBRARY_ITEM_TYPE","description":"Library Item Type"}}},{"caption":"Specification Editing and Discovery Assistant, Phase II","file":{"fileExtension":"png","fileId":298810,"fileName":"SBIR_2012_2_BC_A1.06-9692","fileSize":63720,"objectId":295344,"objectType":{"lkuCodeId":889,"code":"LIBRARY_ITEMS","description":"Library Items","lkuCodeTypeId":182,"lkuCodeType":{"codeType":"OBJECT_TYPE","description":"Object Type"}},"objectTypeId":889,"fileSizeString":"62.2 KB"},"files":[{"fileExtension":"png","fileId":298810,"fileName":"SBIR_2012_2_BC_A1.06-9692","fileSize":63720,"objectId":295344,"objectType":{"lkuCodeId":889,"code":"LIBRARY_ITEMS","description":"Library Items","lkuCodeTypeId":182,"lkuCodeType":{"codeType":"OBJECT_TYPE","description":"Object Type"}},"objectTypeId":889,"fileSizeString":"62.2 KB"}],"id":295344,"title":"Briefing Chart Image","description":"Specification Editing and Discovery Assistant, Phase II","libraryItemTypeId":1095,"projectId":17806,"primary":true,"publishedDateString":"","contentType":{"lkuCodeId":1095,"code":"IMAGE","description":"Image","lkuCodeTypeId":341,"lkuCodeType":{"codeType":"LIBRARY_ITEM_TYPE","description":"Library Item Type"}}},{"caption":"Specification Editing and Discovery Assistant, Phase II Project Image","file":{"fileExtension":"bmp","fileId":304429,"fileName":"SBIR_12_2_A1.06-9692","fileSize":272054,"objectId":300981,"objectType":{"lkuCodeId":889,"code":"LIBRARY_ITEMS","description":"Library Items","lkuCodeTypeId":182,"lkuCodeType":{"codeType":"OBJECT_TYPE","description":"Object Type"}},"objectTypeId":889,"fileSizeString":"265.7 KB"},"files":[{"fileExtension":"bmp","fileId":304429,"fileName":"SBIR_12_2_A1.06-9692","fileSize":272054,"objectId":300981,"objectType":{"lkuCodeId":889,"code":"LIBRARY_ITEMS","description":"Library Items","lkuCodeTypeId":182,"lkuCodeType":{"codeType":"OBJECT_TYPE","description":"Object Type"}},"objectTypeId":889,"fileSizeString":"265.7 KB"}],"id":300981,"title":"Final Summary Chart Image","description":"Specification Editing and Discovery Assistant, Phase II Project Image","libraryItemTypeId":1095,"projectId":17806,"primary":false,"publishedDateString":"","contentType":{"lkuCodeId":1095,"code":"IMAGE","description":"Image","lkuCodeTypeId":341,"lkuCodeType":{"codeType":"LIBRARY_ITEM_TYPE","description":"Library Item Type"}}}],"transitions":[{"transitionId":64294,"projectId":17806,"partner":"Other","transitionDate":"2014-04-01","path":"Advanced From","relatedProjectId":16727,"relatedProject":{"acronym":"","projectId":16727,"title":"Specification Editing and Discovery Assistant","startTrl":2,"currentTrl":7,"endTrl":7,"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.","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.","startYear":2013,"startMonth":5,"endYear":2013,"endMonth":11,"statusDescription":"Completed","website":"","program":{"acronym":"SBIR/STTR","active":true,"description":"
The NASA SBIR and STTR programs fund the research, development, and demonstration of innovative technologies that fulfill NASA needs as described in the annual Solicitations and have significant potential for successful commercialization. If you are a small business concern (SBC) with 500 or fewer employees or a non-profit RI such as a university or a research laboratory with ties to an SBC, then NASA encourages you to learn more about the SBIR and STTR programs as a potential source of seed funding for the development of your innovations.
The SBIR and STTR programs have 3 phases:
The SBIR and STTR Phase I contracts last for 6 months with a maximum funding of $125,000, and Phase II contracts last for 24 months with a maximum funding of $750,000 - $1.5 million.
Opportunity for Continued Technology Development Post-Phase II:
The NASA SBIR/STTR Program currently has in place two initiatives for supporting its small business partners past the basic Phase I and Phase II elements of the program that emphasize opportunities for commercialization. Specifically, the NASA SBIR/STTR Program has the Phase II Enhancement (Phase II-E) and Phase II eXpanded (Phase II-X) contract options.
Please review the links below to obtain more information on the SBIR/STTR programs.
Provides an overview of the SBIR and STTR programs as implemented by NASA
Provides access to the annual SBIR/STTR Solicitations containing detailed information on the program eligibility requirements, proposal instructions and research topics and subtopics
Schedule and links for the SBIR/STTR solicitations and selection announcements
Federal and non-Federal sources of assistance for small business
Search our complete archive of awarded project abstracts to learn about what NASA has funded
Still have questions? Visit the program FAQs
","programId":73,"responsibleMd":{"acronym":"STMD","canUserEdit":false,"city":"","external":false,"linkCount":0,"organizationId":4875,"organizationName":"Space Technology Mission Directorate","organizationType":"NASA_Mission_Directorate","naorganization":false,"organizationTypePretty":"NASA Mission Directorate"},"responsibleMdId":4875,"stockImageFileId":36648,"title":"Small Business Innovation Research/Small Business Tech Transfer"},"lastUpdated":"2024-1-10","releaseStatusString":"Released","viewCount":386,"endDateString":"Nov 2013","startDateString":"May 2013"},"infoText":"Advanced from another project within the program","infoTextExtra":"Another project within the program (Specification Editing and Discovery Assistant)","dateText":"April 2014"},{"transitionId":64295,"projectId":17806,"transitionDate":"2016-04-01","path":"Closed Out","details":"Specification Editing and Discovery Assistant, Phase II Project Image","closeoutDocuments":[{"title":"Final Summary Chart Image","file":{"fileExtension":"bmp","fileId":304799,"fileName":"SBIR_12_2_A1.06-9692","fileSize":272054,"objectId":64295,"objectType":{"lkuCodeId":1841,"code":"TRANSITION_FILES","description":"Transition Files","lkuCodeTypeId":182,"lkuCodeType":{"codeType":"OBJECT_TYPE","description":"Object Type"}},"fileSizeString":"265.7 KB"},"transitionId":64295,"fileId":304799}],"infoText":"Closed out","infoTextExtra":"","dateText":"April 2016"}],"primaryImage":{"file":{"fileExtension":"png","fileId":298810,"fileSizeString":"0 Byte"},"id":295344,"description":"Specification Editing and Discovery Assistant, Phase II","projectId":17806,"publishedDateString":""},"responsibleMd":{"acronym":"STMD","canUserEdit":false,"city":"","external":false,"linkCount":0,"organizationId":4875,"organizationName":"Space Technology Mission Directorate","organizationType":"NASA_Mission_Directorate","naorganization":false,"organizationTypePretty":"NASA Mission Directorate"},"program":{"acronym":"SBIR/STTR","active":true,"description":"The NASA SBIR and STTR programs fund the research, development, and demonstration of innovative technologies that fulfill NASA needs as described in the annual Solicitations and have significant potential for successful commercialization. If you are a small business concern (SBC) with 500 or fewer employees or a non-profit RI such as a university or a research laboratory with ties to an SBC, then NASA encourages you to learn more about the SBIR and STTR programs as a potential source of seed funding for the development of your innovations.
The SBIR and STTR programs have 3 phases:
The SBIR and STTR Phase I contracts last for 6 months with a maximum funding of $125,000, and Phase II contracts last for 24 months with a maximum funding of $750,000 - $1.5 million.
Opportunity for Continued Technology Development Post-Phase II:
The NASA SBIR/STTR Program currently has in place two initiatives for supporting its small business partners past the basic Phase I and Phase II elements of the program that emphasize opportunities for commercialization. Specifically, the NASA SBIR/STTR Program has the Phase II Enhancement (Phase II-E) and Phase II eXpanded (Phase II-X) contract options.
Please review the links below to obtain more information on the SBIR/STTR programs.
Provides an overview of the SBIR and STTR programs as implemented by NASA
Provides access to the annual SBIR/STTR Solicitations containing detailed information on the program eligibility requirements, proposal instructions and research topics and subtopics
Schedule and links for the SBIR/STTR solicitations and selection announcements
Federal and non-Federal sources of assistance for small business
Search our complete archive of awarded project abstracts to learn about what NASA has funded
Still have questions? Visit the program FAQs
","programId":73,"responsibleMd":{"acronym":"STMD","canUserEdit":false,"city":"","external":false,"linkCount":0,"organizationId":4875,"organizationName":"Space Technology Mission Directorate","organizationType":"NASA_Mission_Directorate","naorganization":false,"organizationTypePretty":"NASA Mission Directorate"},"responsibleMdId":4875,"stockImageFileId":36648,"title":"Small Business Innovation Research/Small Business Tech Transfer"},"leadOrganization":{"canUserEdit":false,"city":"Ithaca","congressionalDistrict":"New York 19","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"external":true,"linkCount":0,"organizationId":3456,"organizationName":"GrammaTech, Inc.","organizationType":"Industry","stateTerritory":{"abbreviation":"NY","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"name":"New York","stateTerritoryId":55},"stateTerritoryId":55,"ein":"311582371 ","uei":"CBXRSPNRF8F9","naorganization":false,"organizationTypePretty":"Industry"},"supportingOrganizations":[{"acronym":"LaRC","canUserEdit":false,"city":"Hampton","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"external":false,"linkCount":0,"organizationId":4852,"organizationName":"Langley Research Center","organizationType":"NASA_Center","stateTerritory":{"abbreviation":"VA","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"name":"Virginia","stateTerritoryId":7},"stateTerritoryId":7,"naorganization":false,"organizationTypePretty":"NASA Center"}],"statesWithWork":[{"abbreviation":"NY","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"name":"New York","stateTerritoryId":55},{"abbreviation":"VA","country":{"abbreviation":"US","countryId":236,"name":"United States"},"countryId":236,"name":"Virginia","stateTerritoryId":7}],"lastUpdated":"2024-1-10","releaseStatusString":"Released","viewCount":419,"endDateString":"Apr 2016","startDateString":"Apr 2014"}}