Specification Editing and Discovery Assistant, Phase II

Metadata Updated: February 28, 2019

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.

Access & Use Information

Public: This dataset is intended for public access and use. License: U.S. Government Work

Downloads & Resources


Metadata Created Date August 1, 2018
Metadata Updated Date February 28, 2019

Metadata Source

Harvested from NASA Data.json

Additional Metadata

Resource Type Dataset
Metadata Created Date August 1, 2018
Metadata Updated Date February 28, 2019
Publisher Space Technology Mission Directorate
Unique Identifier TECHPORT_17806
Maintainer Email
Public Access Level public
Bureau Code 026:00
Metadata Context https://project-open-data.cio.gov/v1.1/schema/catalog.jsonld
Metadata Catalog ID https://data.nasa.gov/data.json
Schema Version https://project-open-data.cio.gov/v1.1/schema
Catalog Describedby https://project-open-data.cio.gov/v1.1/schema/catalog.json
Harvest Object Id 6e908d3c-347c-4950-ab6f-76a998faa4fc
Harvest Source Id 39e4ad2a-47ca-4507-8258-852babd0fd99
Harvest Source Title NASA Data.json
Data First Published 2016-04-01
Homepage URL https://techport.nasa.gov/view/17806
License http://www.usa.gov/publicdomain/label/1.0/
Data Last Modified 2018-07-19
Program Code 026:027
Source Datajson Identifier True
Source Hash d9cb5ab5086e5e06a3898615abed7e63ff9ad4d1
Source Schema Version 1.1

Didn't find what you're looking for? Suggest a dataset here.