search menu icon-carat-right cmu-wordmark

Model-Based Verification: Guidelines for Generating Expected Properties

January 2002 Technical Note
David P. Gluch, Santiago Comella-Dorda, John J. Hudak, Grace Lewis, Charles B. Weinstock

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

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.