NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Developing Formal Correctness Properties from Natural Language RequirementsThis viewgraph presentation reviews the rationale of the program to transform natural language specifications into formal notation.Specifically, automate generation of Linear Temporal Logic (LTL)correctness properties from natural language temporal specifications. There are several reasons for this approach (1) Model-based techniques becoming more widely accepted, (2) Analytical verification techniques (e.g., model checking, theorem proving) significantly more effective at detecting types of specification design errors (e.g., race conditions, deadlock) than manual inspection, (3) Many requirements still written in natural language, which results in a high learning curve for specification languages, associated tools and increased schedule and budget pressure on projects reduce training opportunities for engineers, and (4) Formulation of correctness properties for system models can be a difficult problem. This has relevance to NASA in that it would simplify development of formal correctness properties, lead to more widespread use of model-based specification, design techniques, assist in earlier identification of defects and reduce residual defect content for space mission software systems. The presentation also discusses: potential applications, accomplishments and/or technological transfer potential and the next steps.
Document ID
20060051681
Document Type
Preprint (Draft being sent to journal)
External Source(s)
Authors
Nikora, Allen P.
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Date Acquired
August 23, 2013
Publication Date
January 1, 2006
Subject Category
Systems Analysis And Operations Research
Meeting Information
NASA OSMA Software Assurance Symposium(Chest Lake, WV)
Distribution Limits
Public
Copyright
Other
Keywords
requirements engineering
formal specifications
natural language processing
No Preview Available