Formal Modeling And Verification Of Smart Home Care Systems

Smart home care systems are life-critical, so it is very necessary to ensure the correctness, safety and other properties of these systems before deploying them. At present, to verify systems mainly adopts traditional verification methods or formal methods. Traditional verification methods,such as simulation or test,are expensive, and can’t cover all possible situations, therefore can’t guarantee properties of systems. Formal methods can overcome above shortcomings of traditional verification methods by modeling systems and automatic verification of system models.In this paper, a formal analysis method for smart home care systems was proposed to discover design flaws of smart home care systems and ensure the correctness and other properties of smart home care systems.Firstly, a formal modeling framework for smart home care systems was proposed on the basis of existing researches, respectively, from system environment and system design aspects of smart home care systems.Secondly, to find flaws of system design and provide the basis for improving system, the critical attributes of smart home care systems were extracted, and analyzed how to model them according to the characteristics of different attributes.Finally, to demonstrate the feasibility and effectiveness of the method of this paper, it is applied to a case study of a smart home care system designed for people with Alzheimer’s disease, which is named SHCSFAP. And we verify the model of SHCSFAP in PAT(Process Analysis Toolkit) which is an enhanced simulation and model checking tool. Experiment results show that the method proposed in this paper in analyzing and verifying smart care systems is effective.Compared with the prior studies, this method supports for automated verification of smart home care systems and modeling layered and real-time characteristics of smart home care systems by using STCSP(Stateful Timed CSP), LTL(Linear Temporal Logic), PAT. Besides, this method extracted the critical attributes of smart home care systems and discussed how to model and verify them.