Toward a design model-oriented methodology to ensure QoS of a cyber-physical healthcare system

The aging of the world population and its serious consequences have made the development of systems adapted to the needs of seniors an absolute necessity. In recent years, technological improvements have favored the development of efficient healthcare systems, comprising several tiny and very efficient devices that can collect several data (videos, images, scalars, etc.) related to the activity and health of older adults. However, deploying such critical and complex systems raises some crucial issues, particularly security and reliability. Because they handle sensitive data, and a failure in the functioning of the process could lead to the loss of human lives. Within our developed system, named Family Heroes, we present in this paper a methodology for verifying its security and reliability in terms of correct functioning. Our proposed methodology is based on the CATWOE method for analyzing, UML and UML profile MARTE for modeling, and finally UPPAAL model checker for verification. The formal verification results of our Family Heroes System properties guarantee its security and reliability.