Automatic Analysis And Verification Of TAP Rules:An Environment Modeling Based Approach

With the wide application of the IoT services in many fields such as smart home and smart city,Trigger-Action Programming(TAP)is widely used as an end-user programming mechanism for users to customize personalized requirements.However,since the users are lack of programming experience,the TAP rules they wrote have many problems,such as conflict,safety,and privacy issues.Moreover,due to the requirements of energy saving and emission reduction,it is necessary to analyze energy consumption and comfort based on TAP rules.Existing researches have proposed corresponding verification methods for the problems that may be caused by improper TAP rules.However,most of these studies only verify part of the problems,without comprehensive analysis and energy consumption and user comfort analysis.This thesis proposes an automatic analysis and verification of TAP rules based on environment modeling.It defines static analysis and dynamic analysis methods supporting verification of properties such as conflict,safety,and privacy,and provides analysis of energy consumption and user comfort.The main contributions include:We propose a two-layer environment model for IoT environment modeling.We build the IoT environment model from the meta-model layer and the model layer.The meta-model layer introduces modeling elements and their relationships,and the model layer provides accurate models of various entities.Finally,we provide instantiation method for environment models according to the characteristics of various models.We propose a static analysis method based on the dependency relationship between TAP rules.Based on the environment model and instance information,the dependency relationship between TAP rules is extracted and the information flow graph is automatically generated.Accordingly,unused rule,redundant rule,loop rules,rule incompleteness and conflicting rules are transformed into the search problem of the information flow graph.We propose a dynamic analysis method based on simulation trace.We transform TAP rules into SHAs,generate system model automatically with environment model instances,and generate simulation scenarios based on system model.By analyzing the simulation trace of multiple scenarios,the conflict,safety,and privacy problems are verified,and the errors are located.By analyzing the simulation trace of single scenario,the analysis of energy consumption and user comfort is realized.In order to support the proposed method,we implement a tool TAPs-Simulator for automatic analysis and verification of TAP rules based on environment modeling.We apply it to a smart home case to prove the feasibility of the proposed method.To highlight advantages of our approach,we design several groups of comparative experiments to evaluate the capability and efficiency of our approach.The evaluation results show that,although the efficiency is not high,our approach can provide comprehensive analysis and verification of TAP rules,and can provide analysis of energy consumption and comfort.It has strong analysis and verification ability.