Portal de Periódicos da CAPES

Automatic Generation of Specification from Natural Language Based on Temporal Logic

2021; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-77474-5_11

1611-3349

Xiaobing Wang, Li Ge, Chunyi Li, Liang Zhao, Xinfeng Shu,

Model-Driven Software Engineering Techniques

Formal specifications are usually used for describing safety system properties and play an important role in formal verification. In order to improve the effectiveness of formal specification generation and formal verification, this paper proposes a framework for automatic conversion from natural language describing properties to temporal logic formulas, and implements a tool PPTLGenerator (Propositional Projection Temporal Logic formula Generator) for the conversion. First, PPTLGenerator is developed based on JavaCC for automatic conversion from natural language to PPTL. Then, the satisfiability of a PPTL formula generated by PPTLGenerator is checked by a tool PPTLSAT. Finally, to illustrate the principle and effectiveness of the framework, a case study of the safety property of Level 3 autonomous car is provided.