|
Model-Validation in Model-Based Development
|
|
Point of Contact
|
Kurt Woodham
Kurt.Woodham@L-3Com.com
|
|
Dates
|
January 2007 - December 2009
|
|
Problem
|
Since there is an increased reliance on code-generation in model-based development, it is imperative that the models have been adequately validated. Currently, the adequacy of model validation is inferred indirectly by examining test-coverage on the model - there is no direct measure of how well the required model behavior has been validated. We propose techniques to objectively measure the model-validation efforts by systematically measure coverage of the required model-behavior as captured in formal properties. We will (1) define coverage metrics for model-validation, (2) develop tools to measure the coverage of required model behavior, (3) develop tools that can assist in the generation of model-validation tests, and (4) evaluate the efficacy of our work for future NASA projects.
|
|
Objective
|
The project objectives are threefold, (1) basic research, (2) empirical evaluation, and (3) technology transfer and demonstration.First, the research objectives of the project will be met and considered successful if we can: - Define a collection of objective model validation adequacy metrics for a commonly used behavioral specification language such as Linear Time temporal Logic (LTL) and commonly used languages that can be used to encode required model behavior such as Simulink and Stateflow. These criteria must form a spectrum ranging from the very weak (one test per required behavior) to the very strong (some notion of MC/DC coverage over behavioral specifications).
- Develop coverage measurement tools that can be used to assess the model-validation efforts. These tools must be of production quality so that they can - if successful?be adopted in future NASA projects.
- Demonstrate feasibility on a pilot project from the aerospace or avionics domain. We do not view technology transfer as part of the research goals; the technology transfer issue is ad-dressed separately.
We aim to have the validation adequacy metrics defined by June 30, 2007; the implementation of the prototype metric measurement tools by December 31, 2007; the pilot project completed by June 30, 2008; and the final version of the tools ready June, 2009. Second, the objective with the empirical evaluation is to assess the effectiveness of various model-validation metrics; if we provide certain coverage of a metric, is our validation effort likely to reveal flaws in the production system? The empirical portion of our proposed project will be successful if we can conduct our studies on realistic systems. We have access to several NASA relevant systems from the avionics domain and hope to acquire additional systems from ongoing NASA projects (both from the IV&V Facility and the Automated Software Engineering Group at NASA Ames). Hopefully, the empirical work will indicate that the notion of model-validation metrics is suitable for helping us derive effective test-suites for our models; but, this is not guaranteed - this is why the empirical studies are needed. We aim to have the first empirical study completed in conjunction with our pilot project June 30, 2008; following empirical studies will be delivered every 6 months, December 31, 2008 and June 30, 2009. The relatively long time allocated for the studies account for the expected effort in acquiring suitable projects and modeling the requirements. Finally, we aim to transfer the technology - if deemed effective through empirical studies - to at least one ongoing NASA project. We aim to involve on project in the last empirical study and preliminary report on the technology transfer success (or failure) on June 30, 2009 and finally on December 31, 2009.
|
|
Results
|
SAS_07_ExecBrief_MBD_07-193_Woodham.ppt
SAS_07_Tech_Pres_MBD_07-200_Woodham.ppt
|
|
Keywords
|
Software engineering, metrics, testing, requirements, black-box testing, requirements-based testing, test-generation, verification, validation
|
|
Categories
|
Formal Methods
|
|
