The Most Abstract Common Refinement

Abstract

We introduce a novel binary operation on specifications. The most abstract common refinement (m.a.c.r.) of two specifications P1 and P2 is the most abstract specification that refines both P1 and P2. We define the m.a.c.r.s of omega-automata and of linear temporal formulae. The m.a.c.r. operation supports a two-dimensional system design process that combines structural decomposition with stepwise refinement. As an example, we design and verify a watch in several steps, each of which simultaneously integrates and refines two partial specifications of the watch.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 04, 1994
Accession Number
ADA278870

Entities

People

  • Limor Fix
  • Thomas Henzinger

Organizations

  • Cornell University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Alphabets
  • Automata
  • Computer Science
  • Computers
  • Decomposition
  • Information Processing
  • Language
  • Military Research
  • Neurobehavioral Manifestations
  • Sequences
  • Specifications
  • Standards
  • Structural Components
  • Transitions
  • Two Dimensional

Readers

  • Electrical Engineering
  • Mathematical Modeling and Probability Theory.