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

Digital Library

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 February 18, 2019, 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

BibTex

@techreport{GluchModelBasedVerification2002,
title={Model-Based Verification: Guidelines for Generating Expected Properties},
author={David Gluch and Santiago Comella-Dorda and John Hudak and Grace Lewis and Charles Weinstock},
year={2002},
number={CMU/SEI-2002-TN-003},
institution={Software Engineering Institute, Carnegie Mellon University},
address={Pittsburgh, PA},
url={http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5869} }