Enabling correct design and formal analysis of Ambient Assisted Living systems

被引：19

作者：

Benghazi, Kawtar ^{[1
]}

Hurtado, Maria V. ^{[1
]}

Hornos, Miguel J. ^{[1
]}

Rodriguez, Maria L. ^{[1
]}

Rodriguez-Dominguez, Carlos ^{[1
]}

Pelegrina, Ana B. ^{[1
]}

Rodriguez-Fortiz, Maria J. ^{[1
,2
]}

机构：

[1] Univ Granada, Software Engn Dept, Ceuta, Spain

[2] Univ Granada, GEDES Res Grp, Ceuta, Spain

来源：

JOURNAL OF SYSTEMS AND SOFTWARE | 2012年 / 85卷 / 03期

关键词：

AAL; Ambient Assisted Living; Formal methods; Time-constraints; Verification; Validation;

D O I：

10.1016/j.jss.2011.05.022

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：498 / 510

页数：13