Research On The Transformation Method From Natural Language Text To PPTL Formula

With the extensive use of computer technology in various industries,a variety of application software have penetrated into all aspects of social life.Software security is closely related to nation,life,property and privacy security.How to solve the lack of reliability and security caused by software vulnerabilities and errors has been regarded as a hot issue in academia and industry.Formal methods rely on strict mathematical theories,which are suitable for the modeling and verification of hardware and software systems.Their purpose is to improve the reliability and security of hardware and software systems design,and they have been highly regarded by industry.As an important technology in formal methods,model checking uses modeling languages to model the system to be verified and uses formal specifications to define system properties.It searches exhaustively the state space of system model to check the satisfiability of formal specifications.In model checking,there are strict demands for users to define formal specifications.Ordinary users do not have the knowledge background of formal methods,and they prefer to use natural language to describe the properties of the system.For the purpose of defining property specifications that conform to formula syntax and expected semantics,users need to go through a long-term strict training,which limits the application of model checking technology in software and hardware systems security verification of various industries.In order to help users extract formal specifications from the properties of natural language description for model checking,this thesis proposes an automatic method for generating formal specifications of PPTL(Propositional Projection Temporal Logic)from natural language texts.The specific process of the method is as follows: Firstly,the method uses natural language processing technology to parse the properties of natural language description and generates a grammar tree.In order to eliminate the influence of structural ambiguity in the grammar tree,the method traverses the tree to extract,rearrange and tag sentence components,and generates marked texts.Secondly,we put forward a conversion step from marked texts to PPTL formulas.It analyzes the syntax and semantics of marked texts,generates a syntax tree containing clauses,conjunctions and temporal information,and then uses the PPTL formula generation algorithm to traverse the syntax tree to get atomic propositions and a combined PPTL formula.Thirdly,based on the technologies of Stanford NLP,Word Net and Java CC,we implement a tool PPTLGenerator to convert natural language texts into PPTL formulas,which integrates PPTLSAT to determine the satisfiability of the generated formulas.Finally,we use PPTLGenerator to generate a PPTL formula from the property of L3 autonomous vehicle takeover behavior,and carry out the formula generation experiment on a test dataset.The results show that the method is feasible and effective,and has a high formula generation validity.