The increasing proportion of elderly adults across the world calls for Ambient Assisted Living (AAL) solutions that can support the elderly in their daily activities, ensure timely resolution of critical scenarios, and help them live independently and without social isolation. However, most of the existing AAL solutions deliver only certain functionalities, that, if used side by side, cannot resolve potentially critical scenarios in a timely manner. A safe mitigation of such situations is possible if all relevant AAL functions are seamlessly integrated, and supported by artificially intelligent decision-making solutions. Moreover, given the safety-critical nature of such systems, evidence of their correctness and quality of service needs to also be provided via formal analysis techniques. This paper addresses such issues by presenting the ongoing Ph.D. research work of the author, aiming at developing a formally assured ecosystem for AAL systems.