Title
Enabling correct design and formal analysis of Ambient Assisted Living systems
Abstract
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.
Year
DOI
Venue
2012
10.1016/j.jss.2011.05.022
Journal of Systems and Software
Keywords
Field
DocType
aal system,numerous non-functional,conventional approach,non-functional requirement,correct design,deadlock freeness,correct functioning,formal analysis,cardiac alteration,verification approach,emergency assistance system,uml-rt model,formal methods,verification
Living systems,Computer science,Deadlock,Real-time computing,Formal methods,Semantics
Journal
Volume
Issue
ISSN
85
3
0164-1212
Citations 
PageRank 
References 
19
0.86
15
Authors
7