Analysis of Smart Mobile Applications for Healthcare under Dynamic Context Changes

Smart mobile medical computing systems (SMDCSes), e.g., mobile medical applications use context information from the environment to provide useful and often critical healthcare services such as continuous monitoring and control of blood glucose levels by infusion of insulin. Given the unsupervised nature of operation of SMDCSes, context changes that are unaccounted for can cause unprecedented faults leading to violation of requirements such as safety, energy sustainability and reliability. Analysis of SMDCSes for testing requirements violations necessitates consideration of context dependent interactions between the SMDCS software, represented by discrete operating modes and its environment, represented by non-linear partial differential equations over space and time. An intractable number of context change sequence and lack of closed form solutions to differential equations makes the requirements analysis of SMDCSes a challenging task. This paper proposes a novel technique to analyze SMDCSes taking into account the dynamic changes in the context and the constant interaction of the computing systems with the physical environment. To show the usage of the technique, Ayushman pervasive health monitoring system is considered as an example SMDCS. Analytical results show that practices considered healthy for a person such as mobility may not be beneficial when an SMDCS is controlling health.