Go backward to Parallel Program Composition
Go up to Top
Go forward to Decomposing Complete Systems
Composed Specifications
- Decomposition:
- Environment of each component are the other components.
- Assumption about environment must be stated.
- Assumption must be satisfied by other components.
- Decomposition theorem for system verification by proving
property of high-level specification and properties of each low-level
component.
- Composition:
- Environment is unknown.
- Component satisfies guarantee only under assumption .
- Assumption/guarantuee property -|>+ .
- Composition theorem for reasoning about assumption/guarantee
specifications.
Start with informal presentation.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine