The Generation Of Model And Specification Of Event-Driven Internet Of Things Based On Natural Language Understanding

The Internet of Things(IoT)has penetrated personal life and industrial production,and the emergence of smart devices has brought comfort and convenience to users.However,due to the complexity of the smart home system and the lack of user expertise,the security challenge is becoming more and more severe.Since the smart home system is closely related to the privacy,property,and personal safety of users,it is very important to ensure the safety of the system.Model checking is one of the widely used technologies for the event-driven Io T system verification.Model checking is an automated technique that,given a finite-state model of a system and a formal property,systematically checks whether this property holds for(a given state in)that model.However,model checking technology still faces some challenges when it comes to real Io T systems.First,Io T systems consist of various devices,and the accurate modeling of the devices determines the credibility of the verification results.Currently,the device models are extracted through manual modeling or source code analysis.But most of the models are different from real devices.Few studies have tried to obtain models from the natural language descriptions of devices.Second,properties should be described in a precise and unambiguous manner.This is typically done using a property specification language,and the most common is Linear Temporal Logic(LTL).But ordinary users do not have professional mathematical knowledge and cannot understand or provide formal specifications.They usually describe their expectations/specifications through natural language.These issues greatly limit the application of existing verification tools in real Io T systems.To solve the above problems,the main contributions of this work are as follows:·Aiming at the problem of device modeling,this work proposes an NLP-aided device modeling method using the IFTTT functional descriptions.The method first analyzes the sentences using natural language processing technology to extract the semantic information of each sentence.Then,using word embedding technique and a semantic dictionary,a semantic relatedness evaluation strategy is designed. Different functional classes are obtained by clustering analysis of the functional descriptions.On this basis,we propose a method to extract different model elements to construct a primary model.·Aiming at the problem of the generation of the formal specifications,this work proposes a method for automatically generating LTL specifications for smart home Io T using natural language.The method first analyzes the natural language specifications,then identifies the key nodes in the syntax tree,extracts the semantic information and temporal logic information,and generates a tree-like intermediate representation(IR).Next,semantic templates are leveraged to generate an atomic proposition for each clause in the IR.Finally,we design a depth-first search algorithm to combine the atomic propositions to a complete LTL formula.The method relies on the syntax analysis,but the structural ambiguities in natural language can lead to wrong parser trees.To solve this problem,we design specific ambiguity refining techniques to fix and adapt the error-prone parser tree of the original sentence.·We implement an aided modeling tool and an LTL generation tool.We first design a user study to collect rules and natural language specifications from real users.Then we evaluate the performance of these tools on the IFTTT functional descriptions dataset and the natural language specifications dataset,and use the generated models and LTL specifications to verify the scenarios built by real users.The experimental results show that our tools have good performances in accuracy and efficiency,and the generated models and LTL specifications can be effectively applied to the verification of the Io T systems.