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.
The Most Abstract Common Refinement
CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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.
APPROVED FOR PUBLIC RELEASE