Research Results | Program Model Checking Case Studies and Practitioner's Guide


	Search:	Advanced Search

Code 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.

Program Model Checking Case Studies and Practitioner's Guide
Point of Contact	Thomas Pressburger Thomas.T.Pressburger@nasa.gov
Dates	January 2004 - April 2007
Problem	Program model checking is a verification methodology that uses state-space exploration to evaluate large numbers of potential program behaviors (executions). It can be effective at detecting critical software errors that are difficult to find through testing [1]. While best practices for applying program model checking are emerging, they remain an ad hoc combination of methods for capturing properties, building special purpose test drivers, and modification and abstraction of application code. Also, the effect of design practice on verifiability (including model checking) has not been explored. We propose to assemble these best practices, demonstrate and validate their use in several case studies, and document the results into a Practitioner?s Guide for Program Model Checking.
Objective	Year 1, Analysis & Baseline: Determine critical requirements and verification coverage requirements for JSC's SAFM or another C++ application. Set up test environment for the selected application at ARC, apply and document basic model checking techniques and determine coverage of verification goals. Year 2, Application: Apply and document design for verification measures to enhance results of model checking. Determine improvement in coverage of verification goals. Year 3, Evaluation and documentation: Evaluate application of methods for improving model checking conducted during Year 2. Produce practitioner's guidebook for model checking.
Results	SAS 05 Executive Presentation.ppt End Of Year Briefing.ppt SAS-2005-Penix-Full3.ppt SAS 06 Executive Presentation.ppt SAS 06 Technical Presentation.ppt End of year briefing.ppt End of year briefing.ppt A case study and metrics, before and after improvement for verifiability.doc Practitioner's Guidebook_20070427 _final.pdf Program Model Checking Practitioners Guide (final 1-15-08).pdf
Keywords	Model checking, Software Verification and Validation, Design for verification
Categories	Code Analysis Dynamic Analysis Formal Methods

Curator: Josh Stonestreet
NASA Official: Lisa Montgomery

NASA Privacy, Security, Notices