DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
ADA278870
Title:
The Most Abstract Common Refinement
Corporate Author:
CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE
Report Date:
1994-02-04
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.
Descriptive Note:
Interim rept.
Supplementary Note:
DOI: 10.21236/ADA278870
Pages:
0017
Distribution Statement:
Approved for public release; distribution is unlimited. Document partially illegible.
Contract Number:
N00014-91-J-1219
File Size:
0.93MB
