Advanced Search

Content Type

Topics

Publication Date

Model-Based Verification: Analysis Guidelines

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 Report

Show Citation Formats

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://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5569

IEEE

Lewis. Grace, Comella-Dorda. Santiago, Gluch. David, Hudak. John, and Weinstock. Charles, "Model-Based Verification: Analysis Guidelines," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Note CMU/SEI-2001-TN-028, 2001. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5569

APA

Lewis, Grace., Comella-Dorda, Santiago., Gluch, David., Hudak, John., & Weinstock, Charles. (2001). Model-Based Verification: Analysis Guidelines (CMU/SEI-2001-TN-028). Retrieved July 30, 2014, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5569

CHI

Grace Lewis, Santiago Comella-Dorda, David Gluch, John Hudak, & Charles Weinstock. Model-Based Verification: Analysis Guidelines (CMU/SEI-2001-TN-028). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2001. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5569

MLA

Lewis, Grace., Comella-Dorda, Santiago., Gluch, David., Hudak, John., & Weinstock, Charles. 2001. Model-Based Verification: Analysis Guidelines (Technical Report CMU/SEI-2001-TN-028). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5569