Go backward to Queue Component
Go up to Top
Go forward to Proposition
Conjoining Specifications
- Current Situation
- Specification of complete system.
- Specification of individual component.
- Missing: composition of components.
- Idea: composition is conjunction
- Behavior satisfies both and
- Behavior satisfies and
- Conjunction of component specfications
- CQ CM and CE.
- Complete system is conjunction of component and environemnt.
- Detailed definitions
- CQ exists :
Init and Init
and always [(Q and ()) or Q]
and ICL
- QE Init and always [A]
- QM exists : Init and always [A] and ICL
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine