Model-Based Verification: Abstraction Guidelines

Abstract

Model-Based Verification (MBV) is a systematic approach to finding defects (errors) in software requirements, designs, or code. The approach judiciously incorporates mathematical formalism, in the form of models, to provide a disciplined and logical analysis practice, rather than a "proof of correctness" strategy. This technical note presents a number of abstraction techniques that can be used to build essential models of system behavior in the context of MBV and details a methodology for creating state machine models using those techniques. In building essential models, abstraction is used to hide details and expose the entities, variables, states, and transitions needed to construct a state machine model. Through illustrative examples, this technical note identifies the types of simplifications that are useful and effective, and highlights the importance of the perspective in determining what important elements to include in an abstracted model.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 2002
Accession Number
ADA407774

Entities

People

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

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Ground and Sea Platforms
  • Human Systems
  • Sensors

DTIC Thesaurus Topics

  • Application Software
  • Artifacts
  • Central Processing Units
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Control Systems
  • Engineering
  • Engineers
  • Fault Tolerance
  • Homosexuality
  • Language
  • New York
  • Software Development
  • Specifications
  • User Interface

Fields of Study

  • Computer science
  • Engineering

Readers

  • Artificial Intelligence
  • Computational Modeling and Simulation
  • Organizational Process Management (OPM).