Accession Number:

ADA399228

Title:

Model-Based Verification: Guidelines for Generating Expected Properties

Descriptive Note:

Final rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SOFTWARE ENGINEERING INST

Report Date:

2002-01-01

Pagination or Media Count:

28.0

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE