Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

Technical Note

Model-Based Verification: Guidelines for Generating Expected Properties

  • Abstract

    This report presents a basic set of guidelines to facilitate the generation of expected properties in the context of Model-Based Verification. Expected properties are natural language statements that express characteristics of the behavior of a system-characteristics that are consistent with user expectations. Through model checking, expected properties of a system, formally expressed as claims, are analyzed against the model. This analysis can detect inconsistencies between models of the system and their expected properties and identify potential system defects.

  • Download

Cite This Report

SEI

Gluch, David; Comella-Dorda, Santiago; Hudak, John; Lewis, Grace; & Weinstock, Charles. Model-Based Verification: Guidelines for Generating Expected Properties (CMU/SEI-2002-TN-003). Software Engineering Institute, Carnegie Mellon University, 2002. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5869

IEEE

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

APA

Gluch, David., Comella-Dorda, Santiago., Hudak, John., Lewis, Grace., & Weinstock, Charles. (2002). Model-Based Verification: Guidelines for Generating Expected Properties (CMU/SEI-2002-TN-003). Retrieved December 22, 2014, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5869

CHI

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

MLA

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