Go backward to Parallel Program Composition
Go up to Top
Go forward to Decomposing Complete Systems
Start with informal presentation.
- 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
- Environment is unknown.
- Component satisfies guarantee only under assumption .
- Assumption/guarantuee property -|>+ .
- Composition theorem for reasoning about assumption/guarantee
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine