https://www.mdu.se/

Ambient Assisted Living (AAL) solutions are aimed to assist the elderly in their independent and safe living. During the last decade, the AAL field has witnessed a significant development due to advancements in Information and Communication Technologies, Ubiquitous Computing and Internet of Things. However, a closer look at the existing AAL solutions shows that these improvements are used mostly to deliver one or a few functions mainly of the same type (e.g. health monitoring functions). There are comparatively fewer initiatives that integrate different kinds of AAL functionalities, such as fall detection, reminders, fire alarms, etc., besides health monitoring, into a common framework, with intelligent decision-making that can thereby offer enhanced reasoning by combining multiple events. 

To address this shortage, in this thesis, we propose two different categories of AAL architecture frameworks onto which different functionalities, chosen based on user preferences, can be integrated. One of them follows a centralized approach, using an intelligent Decision Support System (DSS), and the other, follows a truly distributed approach, involving multiple intelligent agents. The centralized architecture is our initial choice, due to its ease of development by combining multiple functionalities with a centralized DSS that can assess the dependency between multiple events in real time. While easy to develop, our centralized solution suffers from the well-known single point of failure, which we remove by adding a redundant DSS. Nevertheless, the scalability, flexibility, multiple user accesses, and potential self-healing capability of the centralized solution are hard to achieve, therefore we also propose a distributed, agent-based architecture as a second solution, to provide the community with two different AAL solutions that can be applied depending on needs and available resources. Both solutions are to be used in safety-critical applications, therefore their design-time assurance, that is, providing a guarantee that they meet functional requirements and deliver the needed quality-of-service, is beneficial. 

Our first solution is a generic architecture that follows the design of many commercial AAL solutions with sensors, a data collector, DSS, security and privacy, database (DB) systems, user interfaces (UI), and cloud computing support. We represent this architecture in the Architecture Analysis and Design Language (AADL) via a set of component patterns that we propose. The advantage of using patterns is that they are easily re-usable when building specific AAL architectures. Our patterns describe the behavior of the components in the Behavioral Annex of AADL, and the error behavior in AADL's Error Annex. We also show various instantiations of our generic model that can be developed based on user requirements. To formally assure these solutions against functional, timing and reliability requirements, we show how we can employ exhaustive model checking using the state-of-art model checker, UPPAAL, and also statistical model-checking techniques with UPPAAL SMC, an extension of the UPPAAL model checker for stochastic systems, which can be employed in cases when exhaustive verification does not scale. The second proposed architecture is an agent-based architecture for AAL systems, where agents are intelligent entities capable of communicating with each other in order to decide on an action to take. Therefore, the decision support is now distributed among agents and can be used by multiple users distributed across multiple locations. Due to the fact that this solution requires describing agents and their interaction, the existing core AADL does not suffice as an architectural framework. Hence, we propose an extension to the core AADL language - The Agent Annex, with formal semantics as Stochastic Transition Systems, which allows us to specify probabilistic, non-deterministic and real-time AAL system behaviors. In order to formally assure our multi-agent system, we employ the state-of-art probabilistic model checker PRISM, which allows us to perform probabilistic yet exhaustive verification.

As a final contribution, we also present a small-scale validation of an architecture of the first category, with end users from three countries (Romania, Poland, Denmark). This work has been carried out with partners from the mentioned countries. 

Our work in this thesis paves the way towards the development of user-centered, intelligent ambient assisted living solutions with ensured quality of service.

With the healthcare practice being increasingly dependent on digital processes and electronic communication, there is a need to support a variety of e-Health applications of different requirements, with respect to connectivity, low latency, and high reliability. The focus of this thesis is on providing formal assurance to systems supporting e-Health applications. Among such systems, this thesis considers: a) Ambient Assisted Living (AAL) Systems, aimed to assist the elderly in their independent and safe living within their homes, and b) healthcare assistance systems that include home, hospital, or emergency e-Health applications, where simultaneous access and communication is critical.

In order to provide formal assurance, one needs to  capture both the structure and behavior of the targeted e-Health systems within models that can be formalized and analyzed by formal methods. Due to only few existing initiatives in the AAL domain that integrate common AAL functionalities such as pulse monitoring, fall detection, as well as fire detection, and remote communication with care-givers, within a generic framework, in this thesis, we propose, as a first contribution, two different categories of AAL architecture frameworks onto which different functionalities, chosen based on user preferences, can be integrated. The first solution follows a centralized approach, using an intelligent Decision Support System, and the second employs a distributed architectural approach, involving multiple intelligent agents. Although centralized solutions are easy to develop, scalability, flexibility, multiple user accesses and potential self-healing are easier to achieve with the distributed, agent-based architecture.  To formally assure these solutions against functional, timing and reliability requirements, as a second contribution, we model the architectures in one of the architecture description languages, namely Architecture Analysis and Design Language, to which we assign semantics in terms of various flavors of transition systems. Consequently, we employ corresponding model checking techniques, such as exhaustive model checking in UPPAAL, statistical model checking in UPPAAL SMC, and probabilistic Model Checking in PRISM, to provide the necessary design-time assurance. 

Our AAL formal frameworks abstract away the communication media and assume communication protocols with fixed delays only. Moreover, their scope is limited to home-based assistance with with no simultaneous/parallel user access. 

Hence, we model next the communication media and expand our scope to target generic e-Health systems supporting home, hospital, and emergency use cases. For such systems, networking capabilities with real-time and reliable communication schemes are essential for service-user connectivity, and resource sharing.

One communication scheme employed in such e-Health applications is the fifth generation of cellular wireless technology, namely, 5G, which offers the possibility of creating network slices that provide independent logical networks, to serve a variety of applications characterized by certain quality-of-service requirements. The network slicing is enabled by the underlying 5G service orchestration capabilities that deal with virtual network function placement, implicit resource assignment, and traffic routing.In this work, we study in detail the service orchestration problem in 5G. As the third contribution, we propose a UML-based framework consisting of: (a) a UML5G Service Orchestration Profile (UML5G-SO) that facilitates modeling service orchestration and network slicing for such 5G-based systems, and (b) associated analysis techniques that back the profile, namely logic-based analysis using the USE tool, and exhaustive model checking via UPPAAL. 

As a final contribution, we propose a tool that integrates UML5G-SO models with UPPAAL, and apply our framework on real use cases of e-Health systems, to provide some experimental evaluation by which we gather useful insights with respect to the framework's practical strengths and weaknesses.

Our work in this thesis paves the way towards the development of healthcare assistance systems with assured quality of service.