Generating Linear Temporal Logics Based on Property Specification Templates

研究成果: Chapter

抄録

Temporal logics are widely used in software verification such as model checking. However, creating temporal logics such as linear temporal logics (LTLs) based on property specifications written in a natural language is difficult due to practitioners’ unfamiliarity with property specifications and notations of temporal logics. Although property specification patterns have been introduced to help write correct temporal logics, creating temporal logics using property specification patterns requires an understanding of the pattern system. Since some patterns are difficult to understand, especially for beginners, and the final temporal logics are usually complicated, creating temporal logics using pattern systems is time consuming and error-prone. Here, we introduce a method to create LTLs based on property specification patterns. We experimentally compare the required time and accuracy of our approach to those using property specification patterns. Our approach can improve the creation of LTLs in terms of speed and accuracy. Although our experiment is implemented in Japanese, the results should be applicable to other languages such as English. We also provide a visualization scheme so that practitioners can understand the generated LTLs and confirm that they are correct.

元の言語English
ホスト出版物のタイトルStudies in Computational Intelligence
出版者Springer-Verlag
ページ1-15
ページ数15
DOI
出版物ステータスPublished - 2020 1 1

出版物シリーズ

名前Studies in Computational Intelligence
850
ISSN(印刷物)1860-949X
ISSN(電子版)1860-9503

Fingerprint

Temporal logic
Specifications
Model checking
Visualization

ASJC Scopus subject areas

  • Artificial Intelligence

これを引用

Luo, W., Washizaki, H., & Fukazawa, Y. (2020). Generating Linear Temporal Logics Based on Property Specification Templates. : Studies in Computational Intelligence (pp. 1-15). (Studies in Computational Intelligence; 巻数 850). Springer-Verlag. https://doi.org/10.1007/978-3-030-26428-4_1

Generating Linear Temporal Logics Based on Property Specification Templates. / Luo, Weibin; Washizaki, Hironori; Fukazawa, Yoshiaki.

Studies in Computational Intelligence. Springer-Verlag, 2020. p. 1-15 (Studies in Computational Intelligence; 巻 850).

研究成果: Chapter

Luo, W, Washizaki, H & Fukazawa, Y 2020, Generating Linear Temporal Logics Based on Property Specification Templates. : Studies in Computational Intelligence. Studies in Computational Intelligence, 巻. 850, Springer-Verlag, pp. 1-15. https://doi.org/10.1007/978-3-030-26428-4_1
Luo W, Washizaki H, Fukazawa Y. Generating Linear Temporal Logics Based on Property Specification Templates. : Studies in Computational Intelligence. Springer-Verlag. 2020. p. 1-15. (Studies in Computational Intelligence). https://doi.org/10.1007/978-3-030-26428-4_1
Luo, Weibin ; Washizaki, Hironori ; Fukazawa, Yoshiaki. / Generating Linear Temporal Logics Based on Property Specification Templates. Studies in Computational Intelligence. Springer-Verlag, 2020. pp. 1-15 (Studies in Computational Intelligence).
@inbook{50a4f46b23514bd3b0d30c69b4b40ac5,
title = "Generating Linear Temporal Logics Based on Property Specification Templates",
abstract = "Temporal logics are widely used in software verification such as model checking. However, creating temporal logics such as linear temporal logics (LTLs) based on property specifications written in a natural language is difficult due to practitioners’ unfamiliarity with property specifications and notations of temporal logics. Although property specification patterns have been introduced to help write correct temporal logics, creating temporal logics using property specification patterns requires an understanding of the pattern system. Since some patterns are difficult to understand, especially for beginners, and the final temporal logics are usually complicated, creating temporal logics using pattern systems is time consuming and error-prone. Here, we introduce a method to create LTLs based on property specification patterns. We experimentally compare the required time and accuracy of our approach to those using property specification patterns. Our approach can improve the creation of LTLs in terms of speed and accuracy. Although our experiment is implemented in Japanese, the results should be applicable to other languages such as English. We also provide a visualization scheme so that practitioners can understand the generated LTLs and confirm that they are correct.",
author = "Weibin Luo and Hironori Washizaki and Yoshiaki Fukazawa",
year = "2020",
month = "1",
day = "1",
doi = "10.1007/978-3-030-26428-4_1",
language = "English",
series = "Studies in Computational Intelligence",
publisher = "Springer-Verlag",
pages = "1--15",
booktitle = "Studies in Computational Intelligence",

}

TY - CHAP

T1 - Generating Linear Temporal Logics Based on Property Specification Templates

AU - Luo, Weibin

AU - Washizaki, Hironori

AU - Fukazawa, Yoshiaki

PY - 2020/1/1

Y1 - 2020/1/1

N2 - Temporal logics are widely used in software verification such as model checking. However, creating temporal logics such as linear temporal logics (LTLs) based on property specifications written in a natural language is difficult due to practitioners’ unfamiliarity with property specifications and notations of temporal logics. Although property specification patterns have been introduced to help write correct temporal logics, creating temporal logics using property specification patterns requires an understanding of the pattern system. Since some patterns are difficult to understand, especially for beginners, and the final temporal logics are usually complicated, creating temporal logics using pattern systems is time consuming and error-prone. Here, we introduce a method to create LTLs based on property specification patterns. We experimentally compare the required time and accuracy of our approach to those using property specification patterns. Our approach can improve the creation of LTLs in terms of speed and accuracy. Although our experiment is implemented in Japanese, the results should be applicable to other languages such as English. We also provide a visualization scheme so that practitioners can understand the generated LTLs and confirm that they are correct.

AB - Temporal logics are widely used in software verification such as model checking. However, creating temporal logics such as linear temporal logics (LTLs) based on property specifications written in a natural language is difficult due to practitioners’ unfamiliarity with property specifications and notations of temporal logics. Although property specification patterns have been introduced to help write correct temporal logics, creating temporal logics using property specification patterns requires an understanding of the pattern system. Since some patterns are difficult to understand, especially for beginners, and the final temporal logics are usually complicated, creating temporal logics using pattern systems is time consuming and error-prone. Here, we introduce a method to create LTLs based on property specification patterns. We experimentally compare the required time and accuracy of our approach to those using property specification patterns. Our approach can improve the creation of LTLs in terms of speed and accuracy. Although our experiment is implemented in Japanese, the results should be applicable to other languages such as English. We also provide a visualization scheme so that practitioners can understand the generated LTLs and confirm that they are correct.

UR - http://www.scopus.com/inward/record.url?scp=85071605507&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85071605507&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-26428-4_1

DO - 10.1007/978-3-030-26428-4_1

M3 - Chapter

AN - SCOPUS:85071605507

T3 - Studies in Computational Intelligence

SP - 1

EP - 15

BT - Studies in Computational Intelligence

PB - Springer-Verlag

ER -