Abstract. This chapter presents a formalization of functional and behavioural requirements, and a refinement of requirements to a design for CoCoME using the Relational Calculus of Object and Component SysOS). We give a model of requirements based on an abstraction of the use cases described in Chapter 3.2. Then the refinement calculus of rCOS is used to derive design models corresponding to the top level designs of Chapter 3.4. We demonstrate how rCOS supports modelling different views and their relationships of the system and the separation of concerns in the development.