Enabling correct design and formal analysis of Ambient Assisted Living systems

Ambient Assisted Living (AAL) systems intend to provide services that enable people with specific needs to live an independent and safe life. Emergency treatment services are critical, time-constrained, and require compliance to numerous non-functional (or quality) requirements. In conventional approaches, often, non-functional requirements are kept outside the modeling scope and as such, their verification is also overlooked. For this reason, the specification and verification of Non-functional requirements (NFR) in this kind of services is a key issue. This paper presents a verification approach based on timed traces semantics and a methodology based on UML-RT models (MEDISTAM-RT) to check the fulfillment of nonfunctional requirements, such as timeliness and safety (deadlock freeness), and to assure the correct functioning of the AAL systems. We validate this approach by its application to an Emergency Assistance System for monitoring people suffering from cardiac alteration with syncope. (C) 2011 Elsevier Inc. All rights reserved.