Model-Based Verification: Analysis Guidelines
• Technical Note
Publisher
Software Engineering Institute
CMU/SEI Report Number
CMU/SEI-2001-TN-028DOI (Digital Object Identifier)
10.1184/R1/6575600.v1Topic or Tag
Abstract
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.
Cite This Technical Note
Lewis, G., Comella-Dorda, S., Gluch, D., Hudak, J., & Weinstock, C. (2001, December 1). Model-Based Verification: Analysis Guidelines. (Technical Note CMU/SEI-2001-TN-028). Retrieved December 31, 2024, from https://doi.org/10.1184/R1/6575600.v1.
@techreport{lewis_2001,
author={Lewis, Grace and Comella-Dorda, Santiago and Gluch, David and Hudak, John and Weinstock, Charles},
title={Model-Based Verification: Analysis Guidelines},
month={{Dec},
year={{2001},
number={{CMU/SEI-2001-TN-028},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6575600.v1},
note={Accessed: 2024-Dec-31}
}
Lewis, Grace, Santiago Comella-Dorda, David Gluch, John Hudak, and Charles Weinstock. "Model-Based Verification: Analysis Guidelines." (CMU/SEI-2001-TN-028). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, December 1, 2001. https://doi.org/10.1184/R1/6575600.v1.
G. Lewis, S. Comella-Dorda, D. Gluch, J. Hudak, and C. Weinstock, "Model-Based Verification: Analysis Guidelines," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Note CMU/SEI-2001-TN-028, 1-Dec-2001 [Online]. Available: https://doi.org/10.1184/R1/6575600.v1. [Accessed: 31-Dec-2024].
Lewis, Grace, Santiago Comella-Dorda, David Gluch, John Hudak, and Charles Weinstock. "Model-Based Verification: Analysis Guidelines." (Technical Note CMU/SEI-2001-TN-028). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Dec. 2001. https://doi.org/10.1184/R1/6575600.v1. Accessed 31 Dec. 2024.
Lewis, Grace; Comella-Dorda, Santiago; Gluch, David; Hudak, John; & Weinstock, Charles. Model-Based Verification: Analysis Guidelines. CMU/SEI-2001-TN-028. Software Engineering Institute. 2001. https://doi.org/10.1184/R1/6575600.v1