 |
||
|
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.
|
| Integrating Model Checking and Procedural Languages | |
| Point of Contact |
David Owen David.R.Owen@ivv.nasa.gov |
| Dates | September 2003 - July 2004 |
| Problem | Automatic verification of software models will not scale to large systems, because the huge amount of memory required severely limits what can be modeled, and the whole system must be rewritten in the model, which is not practical when otherwise convenient open-source code is borrowed and reused. |
| Objective | Develop (from working prototype) an alternative automatic verification tool without such severe memory limitations, a tool which allows as-is code to make up part of the model, but provides close to the same functionality now provided by other model-based verification tools. |
| Results |
Summary Report and SAS Presentation.ppt Training Session 1.ppt Lurch Version 1 and Documentation.zip Task Project Plan.xls Goals for Lurch Version 2.pdf |
| Keywords | model checking, error checking, software testing, model based verification, LURCH |
| Categories |
Code Analysis Design Analysis Domain-Specific Analysis Formal Methods |
|
| |
|
Curator: Josh Stonestreet NASA Official: Lisa Montgomery |
|
NASA Privacy, Security, Notices |