Model-Based Verification: Claim Creation Guidelines

Abstract

Model Based Verification (MBV) is a systematic approach to finding defects (errors) in software requirements, designs, or code. MBV involves creating essential models of system behavior and analyzing these models against formal representations of expected properties, known as claims. Claim generation has been identified as a particularly complex activity within model-based verification. This technical note describes a pattern-based approach to facilitate claim generation. The report includes a list of directly usable patterns for the most frequent expected properties found in system specifications.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 2001
Accession Number
ADA396125

Entities

People

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

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Air Platforms
  • Weapons Technologies

DTIC Thesaurus Topics

  • Computer Programming
  • Computer Science
  • Computers
  • Demographic Cohorts
  • Engineering
  • Guarantees
  • Homosexuality
  • Language
  • Language Translation
  • Materials
  • Natural Languages
  • New York
  • Programming Languages
  • Software Development
  • Specifications
  • Standards
  • Verification

Fields of Study

  • Computer science

Readers

  • Computational Modeling and Simulation
  • Software Engineering.