Automated Generation of LTL Specifications For Smart Home IoT Using Natural Language
Shiyu Zhang1, Juan Zhai1,2, Lei Bu1, Mingsong Chen2, Linzhang Wang1 and Xuandong Li1
1State Key Laboratory of Novel Software Technology, Department of Computer Science and Technology, Nanjing University
2Department of Computer Science, Rutgers University
3Shanghai Key Lab of Trustworthy Computing, East China Normal University
ABSTRACT
Ordinary users can build their smart home automation system easily nowadays, but such user-customized systems could be error-prone. Using formal verification to prove the correctness of such systems is necessary. However, to conduct formal proof, formal specifications such as Linear Temporal Logic (LTL) formulas have to be provided, but ordinary users cannot author LTL formulas but only natural language. To address this problem, this paper presents a novel approach that can automatically generate formal LTL specifications from natural language requirements based on domain knowledge and our proposed ambiguity refining techniques. Experimental results show that our approach can achieve a high correctness rate of 95.4% in converting natural language sentences into LTL formulas from 481 requirements of real examples.
