2021 Fiscal Year Annual Research Report
A divide and conquer approach to parallelization of LTL model checking
| Project/Area Number |
19H04082
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | モデル検査 / 状態空間爆発 / 分割統治 / 線形時相論理 / Maude |
|---|
| Outline of Annual Research Achievements |
（１）当該年度に予定していた研究実施計画に則り研究を実施し、以下の実績を達成した：
理論研究：pとqを状態命題としたとき、状態空間に対する<> p（Eventual性質）とp |-> [] q（Conditional stable性質）のモデル検査と等価となる状態空間を２以上（L+1、ここでLは正整数）のレイヤーに分割し得られる複数の小さな状態空間に対するモデル検査を行う方法を考案すると共に等価性の証明を行った。アルゴリズムの考案：理論研究で得られる「状態空間をL+1レイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法」に基づきアルゴリズムを設計した。支援ツールの開発：そのアルゴリズムを実現する支援ツールの逐次版と並列版のプロトタイプをMaudeを実装言語として用いて作成した。前年度に作成したLeads-to性質用の支援ツール（逐次版と並列版）のプロトタイプを基に完成版を開発した。事例研究：既存のLTLモデル検査器では状態爆発のためモデル検査不能になる事例を支援ツールの逐次版を用いることでモデル検査可能になること、支援ツールの並列版を用いることでモデル検査の実行速度が改善できることを確認した。研究成果発表：成果を複数の国際会議で発表すると共に国際会議論文を出版した。
（２）当該年度には予定していなかった研究成果を達成した：
本研究で提案する方法は、ソフトウェアの設計のためのモデル検査用であった。プログラムを対象とするソフトウェアモデル検査器であるJava Pathfinder（JPF）を基にJavaで記述した並行プログラムを提案方法でモデル検査する支援ツールを開発し、成果を国際学術誌に発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
予定していたこと以上のことを達成したためである。具体的には、研究で提案する方法は、ソフトウェアの設計のためのモデル検査用であった。プログラムを対象とするソフトウェアモデル検査器であるJava Pathfinder（JPF）を基にJavaで記述した並行プログラムを提案方法でモデル検査する支援ツールを開発し、成果を国際学術誌に発表したためである。
|
| Strategy for Future Research Activity |
理論研究：状態空間を２以上（L+1、ここでLは正整数）のレイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法をLeads-to性質（p |-> q、ここでpとqは状態命題）、Eventual性質（<> p、ここでpは状態命題）及びConditinal stable性質（p |-> [] q、ここでpとqは状態命題）以外のLTL性質に拡張する。候補として、Until性質（p U q、ここでpとqは状態命題）とConditional until生成（p U [] q、ここでpとqは状態命題）を考えている。とういうのは、これらの性質を扱うことができるようになると、Maude線形時相モデル検査器だけでなく、Maudeを拡張し実時間システムの形式仕様を作成したり実時間システムが所望の性質を満たすことのモデル検査をしたりすることのできるReal-Time Maudeに提案方法を応用することが可能になるためである。支援ツールの開発：上述した性質を提案方法でモデル検査するための支援ツール（逐次版と並列版）を開発する。提案方法をReal-Time Maudeに応用し、提案方法で実時間システムが所望の性質を満たすことのモデル検査を提案方法で行うことのできる支援ツールのプロトタイプ（逐次版）を作成する。事例研究：Test&set、Qlock、Anderson、MCSなどの相互排除プロトコルを事例として用い、提案方法・支援ツールの有効性を示す事例研究を行う。研究成果発表：国際会議や国際誌に論文を投稿する。
|
