 |
||
|
Advanced Search |
||
|
|||||
|
Dynamic 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.
|
| Practical Model Checking to Enforce Domain Specific Interfaces | |
| Point of Contact |
Michael Hieber Michael.A.Hieber@saic.com |
| Dates | January 2004 - October 2006 |
| Problem | Domain-specific interfaces and requirements must be checked to ensure the integrity of complex software systems. Today, checking requirements is very time-intensive and expensive because most of it must be done manually. Error-finding tools like FlexeLint are neither powerful enough nor customizable enough to check complicated interface rules. The SPIN model checker only works on finite state machine systems, not C/C++ code. In contrast, push-down model checking is naturally suited to checking C/C++ code because of its stack-based nature. This initiative will explore the use of push-down model-checking technology to automate the checking of domain-specific NASA requirements. |
| Objective | By December 2006, SAIC and GrammaTech will have developed and integrated model-checking queries to automate NASA IV&V inspection tasks. By December 2004, we will have selected a specific NASA project, implemented pilot queries, and tested the queries on the code. By December 2005, additional queries will have been selected, implemented, and evaluated. By December 2006, the queries will have been abstracted so they can easily be adapted to new projects, and the model-checking techniques will be ready for integration into the NASA IV&V process. |
| Results |
04 Software Assurance Symposium presentation.ppt SAS 05 Executive Presentation.ppt Practical Model Checking End of Year Report 2004.doc Report summarizing implementation of queries.ppt SAS 06 Executive Presentation.ppt SAS 06 Technical Presentation.ppt SAS 05 Technical Presentation.ppt Final report..doc List of queries and state-machine code for the queries.ZIP Report on second year's findings - Sanitized for Public Distribution.doc Summary Report for Queries.doc |
| Keywords | Model checking, software assurance, software verification, static analysis, software testing |
| Categories |
Quality Assurance Quality Engineering Code Analysis Dynamic Analysis Interface Analysis Static Analysis |
|
| |
|
Curator: Josh Stonestreet NASA Official: Lisa Montgomery |
|
NASA Privacy, Security, Notices |