IV&V Facility Research Program Results and SARP Results  

Advanced Search
Design Analysis < Verification & Validation < Results Home

Click here to complete a short survey. The results of this survey will be used to help us improve the research program and this website.

Click here to view research projects that had new research results added in the last 90 days.
Developing Formal Correctness Properties from Natural Language Requirements
Point of Contact Allen Nikora
anikora@mail.jpl.nasa.gov
Dates June 2006 - June 2008
Problem Model-based development techniques such as the SPIN model checker have been shown to be effec-tive in identifying types of defects (e.g., deadlocks, race conditions) that cannot be easily detected by manual techniques such as formal inspections, and that can be particularly difficult and expensive to find during the testing phase. If these techniques were to be more widely applied across NASA space mission development efforts, the residual defect content of space mission systems (e.g., on-board command and data handling software) could be significantly decreased, thereby reducing the overall risk of mission failure and prolonging expected mission lifetimes. The proposed work enables more widespread use of model-based development techniques by developing techniques and tools to assist developers in bridging the gap between the informal natural language text commonly used in docu-menting system requirements and the rigorous models needed to reap the benefits of model-based techniques. Specifically, we will address the problem of transforming natural language requirements to rigorously-specified correctness properties against which a formal system model can be checked.
Objective
  1. By 2007/03/01:
    1. Demonstrate improved classifier performance (higher pd, lower pf) in discriminating between natural language temporal and non-temporal requirements (Progress toward this goal should be evident)
    2. Demonstrate the capability for matching the structure of natural language temporal requirements to the appropriate Linear Temporal Logic (LTL) pattern.
    3. Complete the initial specification and design of a toolset for transforming natural language temporal language requirements to LTL expressions.
  2. By 2007/09/01:
    1. Demonstrate the capability for populating an LTL pattern with semantic information from the corresponding natural language requirement text.
    2. Complete the final specification and design of a toolset for transforming natural language temporal language requirements to LTL expressions.
  3. By 2008/03/01:
    1. Implement a toolset for transforming natural language temporal requirements to LTL expressions.
Results SAS 06 Executive Presentation.ppt
SAS 06 Technical Presentation.ppt
SAS07_Exec_Brief_Formal_Specs_Nat_Lang_Nikora.ppt
SAS07_Tech_Pres_Formal_Specs_Nat_Lang_Nikora.ppt
Keywords requirements analysis, natural language processing, model analysis tools, linear temporal logic patterns
Categories Design Analysis
Requirements Analysis


Curator: Josh Stonestreet
NASA Official: Lisa Montgomery
 NASA Insignia NASA Privacy, Security, Notices