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 non-functional 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.

► Systems supporting emergency treatment services are time-constrained.
► Safety and timeliness should be considered since the first systems development steps.
► Timed-constraints systems specified by Medistam-RT are correct-by-construction.
► A timed-constrained system is correct if its basic components are correct.
► Non-functional NFRs and basic components behaviour are mapped to a common domain.