Emerging Ambient Assisted Living (AAL) applications, as a part of AmI applications, deal essentially with health- care related applications such as assistance to the elderly and handicapped persons, emergency services. Several ap- proaches and techniques have been proposed, providing formal languages modeled with ontologies (e.g. OWL-S, WSMO) that describe in semantic way the environment. In this paper, relevant challenges of the current AAL ap- plication development, with a focus on the formal specification and verification are discussed. A formal system which enable to specify a semantic model represented by an upper ontology is presented. The innovative aspect of the proposed model concerns the use of a constructive description logic.