Accession Number:

ADA278870

Title:

The Most Abstract Common Refinement

Descriptive Note:

Interim rept.

Corporate Author:

CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Fix, Limor
• Henzinger, Thomas A.

Report Date:

1994-02-04

Pagination or Media Count:

17.0

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.

Descriptors:

• *COMPUTER LOGIC
• *COMPUTER ARCHITECTURE
• DISTRIBUTED DATA PROCESSING
• PARALLEL PROCESSING
• REFINING
• FIELDS(COMPUTER PROGRAMS)
• AUTOMATA
• BINARY PROCESSORS
• DECOMPOSITION
• CONCURRENT ENGINEERING
• SPECIFICATIONS
• TWO DIMENSIONAL

Subject Categories:

• Computer Hardware
• Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE