In ubiquitous applications, where the meaning of an entity, such as a user or service, depends on environment-specific constraints and dynamic changes in the environment have to be considered in all stages of development, the separation between the system’s behaviour and its context representation (a.k.a. context model) is essential for facilitating the development of such inherently complex systems. At the same time, because of its well-known benefits, a formal specifications should be considered not only for describing the system’s behaviour, but also the corresponding context model. Considering this, we propose in this paper an environment to support context modelling through formal specification. For this sake, we adopt the algebra of contextualized entities proposed in [Comorea2008,Isola2008] and define levels of abstractions over its diagrams, enabling a stepwise construction of modular specifications. The overall goal is to reduce the gap between the formal description of an ubiquitous application and its implementation.