Analyzing Tabular Requirements Specifications Using Infinite State Model Checking

Abstract

This paper investigates the application of infinite state model checking to the formal analysis of requirements specifications in the SCR (Software Cost Reduction) tabular notation using Action Language Verifier (ALV). After reviewing the SCR method and tools and the Action Language, experimental results are presented of formally analyzing two SCR specifications using ALV. The application of ALV to verify or falsify (by generating counterexamples) the state and transition invariants of SCR specifications and to check Disjointness and Coverage properties is described. ALV is compared with the verification techniques that have been integrated into the SCR toolset.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2006
Accession Number
ADA462324

Entities

People

  • Constance Heitmeyer
  • Tevfik Bultan

Organizations

  • United States Naval Research Laboratory

Tags

Communities of Interest

  • Weapons Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Air Traffic Control Systems
  • Arithmetic
  • Automata
  • Composite Materials
  • Computations
  • Consistency
  • Control Systems
  • Demographic Cohorts
  • Formal Languages
  • Iterations
  • Language
  • Military Research
  • Semantics
  • Specifications
  • Standards
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.