Research Results | Tandem Experiments in Finding Faults During Model-Based Development


	Search:	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.

Tandem Experiments in Finding Faults During Model-Based Development
Point of Contact	Kurt Woodham kurt.woodham@titan.com
Dates	January 2004 - December 2006
Problem	Model-based development centers the software development effort on models of the intended software behavior and relies on code generation to produce the production software. Unfortunately, existing V&V analysis processes and tools do not readily accommodate models that contain numeric data variables involved in interrelated constraints ? for example, most control models expressed in languages such as Simulink and SCADE. Such models are being used increasingly for NASA missions such as STEREO. New analysis methods and an expanded V&V toolset are required to effectively perform V&V on flight critical software developed using such models. The effectiveness of existing V&V methods when data variables are present is currently very limited ? this project aims at developing and empirically assessing alternatives to existing techniques.
Objective	Check static knowledge of specifications that use numeric variables Assess the value of using the MAAB guidelines to check NASA MATLAB models. Apply the MABB guidelines to NASA MATLAB models using the MINT toolkit. Check dynamic knowledge of specifications that use numeric variables Extend a temporal properties checker written previously with OSMA funds (LURCH) to handle numeric variables. Test this extended version on many models including NASA?s MATLAB models Where possible, benchmark the above against alternate approaches E.g. manual analysis E.g. conventional model checking such as SPIN or SMV (after abstracting numeric variables to discrete variables). Evaluate our approach for scalability, usability, and maintainability on NASA case models
Results	Report use MAAB on MATLAB model 1.doc Report review utility MAAB for NASA Models.doc SAS CY04 Technical Briefing.ppt SAS CY04 Executive Level Briefing.ppt SAS 05 Executive Presentation.zip Report, Static Analysis Study Summary.doc SAS 06 Executive Presentation.ppt SAS 06 Technical Presentation.ppt Report, use, MAAB, on MATLAB model2.doc SAS 05 Technical Presentation.zip Report, SPY Version 1.0 (Baseline).zip Report, Utility of using Mint on MATLAB Model3.doc Report-SPYCOTS Comparison.doc Final Report.doc Report, Survey of Tools Accessible via Intermediate Translator.pdf
Keywords	Discrete variables, Discrete model, Numeric variables, Numeric model, Hybrid, model, MAAB style, MINT, Temporal Logic, LURCH, MATLAB, Model Checking
Categories	Quality Control Software Reliability Design Analysis Domain-Specific Analysis Dynamic Analysis Formal Methods Interface Analysis Test Analysis

Curator: Josh Stonestreet
NASA Official: Lisa Montgomery

NASA Privacy, Security, Notices