 |
||
|
Advanced Search |
||
|
|||||
|
Domain-Specific 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.
|
| A Compositional Approach to Validation of Formal Models | |
| Point of Contact |
Bojan Cukic cukic@csee.wvu.edu |
| Dates | January 2004 - December 2006 |
| Problem |
Proving the correctness of the developed specification with respect to the requirements is one of the portant and the most difficult tasks performed by NASA IV&V personnel. We will focus on compositional approach of validation of the formal specifications using visualization, simulation, formal methods and testing. The basis of our approach is the SCR (Software Cost Reduction) Formal Method and its finite state model of the system. An SCR specification can be executed by the existing SCR simulator and tested - either automatically (i.e. random testing) or manually. In order to facilitate testing of the specification simulation, we propose to investigate the creation of visual interfaces. The visual interfaces will hide the complexity of the model (and the formal mathematical notations being used) from the users and the domain experts. Performing testing using these visual interfaces would allow the V&V practitioner to focus on the expected behavior of the system and the correctness of the specification.
Based on the coverage of the executed tests, we will explore how to abstract the part of the specification that was thoroughly tested, and perform model checking or further testing on the rest of the specification. Using testing early in the lifecycle on the specification model (simulation) is more cost effective than testing the actual implementation. In fact, NASA IV&V engineers rarely test implementations. Also, testing of the specification model will allow us to decompose the formal model and reduce the number of states. Hence, we hope avoid the state explosion problem while model checking the other parts of the specification. |
| Objective |
|
| Results |
SAS 05 Executive Presentation.ppt SAS 06 Executive Presentation.ppt SAS 06 Technical Presentation.ppt SAS 05 Technical Presentation.ppt Decomposition and Abstraction of SCR specifications based on tests coverage.htm Development of visualization tools for testing of SCR simulations.htm Tracking Test Coverage on SCR specification constructs.htm Compositional Approach using Testing and Model Checking for Verification of SCR specifications.pdf Experimental results on the FPE and other SCR specifications.pdf Verification of the abstracted model by Guided Testing and Model Checking.pdf Final_Report_Desovski_Cukic.pdf SAS_07_ExecBrief_Compositional_Verification_Cukic_v2.ppt SAS_07_Tech_Pres_Compositional_Cukic.ppt Combining Complementary Formal Verification Strategies.pdf An Empirical Investigation of Performance Variations in Formal Verification Experiments.pdf |
| Keywords | |
| Categories |
Quality Control Design Analysis Domain-Specific Analysis Formal Methods Management & Planning of V&V Requirements Analysis |
|
| |
|
Curator: Josh Stonestreet NASA Official: Lisa Montgomery |
|
NASA Privacy, Security, Notices |