3J-03
テンプレートに基づく線形時相論理式の生成手法
○駱　煒賓，鷲崎弘宜，深澤良彰（早大）
　モデル検査においては、検証したい性質を線形時相論理(LTL)式で記述する必要がある。 LTL式を作成するために性質パター用いる手法がある。しかし、既存手法では 線形時相論理や性質パターンに関する知識が不可欠であり、LTL式を作成する際にも多くの時間を必要とする。そのため、より理解しやすいかつ効率的なLTL式生成手法が求められている。
　本研究では、LTL式の作成において、自然言語のテンプレートに基づく線形時相論理式の生成手法を提案する。また、LTL式生成ツールと既存手法を用いて比較実験を行い、以下の研究課題について報告する。
RQ1　LTL式生成ツールによってLTL式作成の時間がどれくらい向上できたか?
RQ2　LTL式生成ツールによってLTL式作成の正確率がどれくらい向上できたか?
footer 著作権について 倫理綱領 プライバシーポリシー セキュリティ 情報処理学会