search menu icon-carat-right cmu-wordmark

Model-Based Verification: Guidelines for Generating Expected Properties

Technical Note
This report presents a basic set of guidelines to facilitate the generation of expected properties in the context of Model-Based Verification.
Publisher

Software Engineering Institute

CMU/SEI Report Number
CMU/SEI-2002-TN-003
DOI (Digital Object Identifier)
10.1184/R1/6575624.v1

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.

Cite This Technical Note

Gluch, D., Comella-Dorda, S., Hudak, J., Lewis, G., & Weinstock, C. (2002, January 1). Model-Based Verification: Guidelines for Generating Expected Properties. (Technical Note CMU/SEI-2002-TN-003). Retrieved May 26, 2024, from https://doi.org/10.1184/R1/6575624.v1.

@techreport{gluch_2002,
author={Gluch, David and Comella-Dorda, Santiago and Hudak, John and Lewis, Grace and Weinstock, Charles},
title={Model-Based Verification: Guidelines for Generating Expected Properties},
month={Jan},
year={2002},
number={CMU/SEI-2002-TN-003},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6575624.v1},
note={Accessed: 2024-May-26}
}

Gluch, David, Santiago Comella-Dorda, John Hudak, Grace Lewis, and Charles Weinstock. "Model-Based Verification: Guidelines for Generating Expected Properties." (CMU/SEI-2002-TN-003). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, January 1, 2002. https://doi.org/10.1184/R1/6575624.v1.

D. Gluch, S. Comella-Dorda, J. Hudak, G. Lewis, and C. Weinstock, "Model-Based Verification: Guidelines for Generating Expected Properties," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Note CMU/SEI-2002-TN-003, 1-Jan-2002 [Online]. Available: https://doi.org/10.1184/R1/6575624.v1. [Accessed: 26-May-2024].

Gluch, David, Santiago Comella-Dorda, John Hudak, Grace Lewis, and Charles Weinstock. "Model-Based Verification: Guidelines for Generating Expected Properties." (Technical Note CMU/SEI-2002-TN-003). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Jan. 2002. https://doi.org/10.1184/R1/6575624.v1. Accessed 26 May. 2024.

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. 2002. https://doi.org/10.1184/R1/6575624.v1