Go backward to The General Theorem
Go up to Top
Go forward to The Composition Theorem
Composing Assumption/Guarantee Specifications
- General form:
- Assertion that system guarantees under assumption that environment
- -|>+ .
- If environment satisfies till time , then system must satisfy
till time .
- Write environment assumptions are safety properties.
- Write systems's fairness guarantee as conjunction of properties
SF(A) where is an environment fairness
- By Proposition 1, resulting specification is machine-closed (if
is machine-closed and , then is machine-closed).
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine