The Formal Analysis And Verification Of Frameworks Of Smart Home Based On PAT

Formal method is a systematic research method based on rigorous mathematical logic. As it is rigorous and accurate, formal method is suitable to solve the problems of concurrency and security in the process of system design and development. Pat(Process Analysis Toolkit) platform is a formal modeling and automatic test tool which is full-featured and easy to use. It has been successfully applied in the modeling and verification of composite behavior of intelligent furniture. Potential errors and shortcomings are found and improved. But it has not formed a general formal model to describe and verify the smart home system.Smart home frameworks refers to the integrated system composited by intelligent device, control program and operating systems to provide the services for users. The device heterogeneity and the importance of safety put forward strict requirements on the correctness and safety of operations. How to automatically detect the exception of operating rules and safety defects have become a problem urgently to be solved.To solve the above issues, we present a construction model of smart home frameworks architecture and provide verification methods of the characteristics of the frameworks through formal modeling and analysis. The abnormal and conflict of the framework can be detected and corrected. The results of experiments show that the model and formal detection method can produce effective results to the application and detection of smart home frameworks.The main contents of this paper include the following parts:First, the analysis of the various components in the composition of smart home frameworks(control apps, accessories controlling framework, common database and intelligent devices), making the function, structure characteristics and communication control method clear, and proposing the smart home frameworks architecture model. Make sure the system demands combined with the practical application.Next, the formal definition of the platform architecture model is given to implement the model description of smart home frameworks. The modules of the platform and its parallel communication are described and modeled. Combined with scenarios, the requirement of the system is described to find the related characteristics of framework, then use formal language to describe the characteristics precisely.Finally, the formal analysis and verification of the architecture model of the smart home platform on the PAT platform are carried out. The experiments included the inspection and improvement of two platform object and platform operation, the results proved the correctness and practicability of the model.