Model-Based Verification: Analysis Guidelines
This technical note provides guidance for the analysis activity that occurs during the interpretation of results produced by model-checking tools. In the model-checking analysis activity, the main question is, "Does the system behave correctly?" To answer this question, a model and a set of expected properties are used as input to a model checker. The expected output is a confirmation or refutation of the specified expected properties. In most cases, if the model checker does not confirm the property, it provides a counterexample.
Counterexamples are executions of the model showing the sequence of steps that refutes the expected property. Sometimes the state space to be explored in order to find this counterexample is so large that it cannot be completely covered. This is the state explosion problem. Models must be tuned to reduce the state space; this is a manual and intuitive task. Interpreting the model checker's output can also be difficult. The significance of the output must be assessed; its interpretation may suggest an error in the claims or the model, or a defect in the actual system.
This document presents the problems related to interpreting results. It provides strategies to overcome state explosion, analyze results, and provide feedback to the system designers and developers.
This report is related to the following area(s) of work:
Performance and DependabilityTechnical Note
CMU/SEI-2001-TN-028
December 2001
Cite This Report
SEI:
Lewis, Grace; Comella-Dorda, Santiago; Gluch, David; Hudak, John; & Weinstock, Charles. Model-Based Verification: Analysis Guidelines (CMU/SEI-2001-TN-028). Software Engineering Institute, Carnegie Mellon University, 2001. http://www.sei.cmu.edu/library/abstracts/reports/01tn028.cfm
IEEE:
G. Lewis, S. Comella-Dorda, D. Gluch, J. Hudak, and C. Weinstock, "Model-Based Verification: Analysis Guidelines," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Note CMU/SEI-2001-TN-028, 2001. http://www.sei.cmu.edu/library/abstracts/reports/01tn028.cfm
APA:
Lewis, G., Comella-Dorda, S., Gluch, D., Hudak, J., & Weinstock, C. (2001). Model-Based Verification: Analysis Guidelines (CMU/SEI-2001-TN-028). Retrieved May 22, 2013, from the Software Engineering Institute, Carnegie Mellon University website: http://www.sei.cmu.edu/library/abstracts/reports/01tn028.cfm
CHI:
Lewis, Grace, Santiago Comella-Dorda, David Gluch, John Hudak, and Charles Weinstock. Model-Based Verification: Analysis Guidelines (CMU/SEI-2001-TN-028). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2001. http://www.sei.cmu.edu/library/abstracts/reports/01tn028.cfm
MLA:
Lewis, G., Comella-Dorda, S., Gluch, D., Hudak, J., & Weinstock, C. 2001. Model-Based Verification: Analysis Guidelines (Technical Report CMU/SEI-2001-TN-028). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://www.sei.cmu.edu/library/abstracts/reports/01tn028.cfm
Find Us Here
Share This Page
For more information
