TY - GEN
T1 - Automated Generation of LTL Specifications for Smart Home IoT Using Natural Language
AU - Zhang, Shiyu
AU - Zhai, Juan
AU - Bu, Lei
AU - Chen, Mingsong
AU - Wang, Linzhang
AU - Li, Xuandong
N1 - Publisher Copyright:
© 2020 EDAA.
PY - 2020/3
Y1 - 2020/3
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85087407657
U2 - 10.23919/DATE48585.2020.9116374
DO - 10.23919/DATE48585.2020.9116374
M3 - 会议稿件
AN - SCOPUS:85087407657
T3 - Proceedings of the 2020 Design, Automation and Test in Europe Conference and Exhibition, DATE 2020
SP - 622
EP - 625
BT - Proceedings of the 2020 Design, Automation and Test in Europe Conference and Exhibition, DATE 2020
A2 - Di Natale, Giorgio
A2 - Bolchini, Cristiana
A2 - Vatajelu, Elena-Ioana
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2020 Design, Automation and Test in Europe Conference and Exhibition, DATE 2020
Y2 - 9 March 2020 through 13 March 2020
ER -