This paper deals with semantic composition of ubiquitous computing (Ubicomp) services in multi-domain heterogeneous environments. A new semantic framework enabling the specification of multidomain composite services and proving their correctness is proposed. The proposed framework reduces the gap between safety critical systems including ubiquitous services and best effort engineering practices. It consists of an extensible Semantic Conceptual Model (SCM) for Ambient Intelligence systems and a composition formal system based on the Basic Constructive Description Logics BCDL0. The soundness property proof of the proposed formal system, as well as, the services composition correctness proofs are demonstrated along with the interactive theorem prover Isabelle/HOL.