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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2002
Accession Number
ADA399228

Entities

People

  • Chick Weinstock
  • David P. Gluch
  • Grace Lewis
  • John J. Hudak
  • Santiago Comella-dorda

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Authentication
  • Classification
  • Computer Programming
  • Computer Science
  • Control Systems
  • Engineering
  • Engineers
  • Formal Languages
  • Homosexuality
  • Language
  • Maintenance Personnel
  • Materials
  • Natural Languages
  • Software Development
  • Standards
  • Students
  • Verification

Fields of Study

  • Computer science

Readers

  • Computational Modeling and Simulation
  • Software Engineering.