2019 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 | モデル検査 / 状態機械 / Leads-to性質 / 分割統治 / 並列化 |
|---|
| Outline of Annual Research Achievements |
（１）当該年度に予定していた研究実施計画に則り研究を実施し、以下の実績を達成した：
理論研究：pとqを状態命題としたとき、状態空間に対してのp |-> qのモデル検査と等価となる、状態空間を２つのレイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法を考案した。等価性の証明を行った。アルゴリズムの考案：理論研究で得られる「状態空間を２つのレイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法」 に基づきアルゴリズムを設計した。支援ツールの開発：そのアルゴリズムを実現するツールを開発した。開発では、書換え論理に基づく計算機言語であるMaudeを用いた。モデル検査の対象となるシステムの仕様もMaudeで作成した。事例研究：相互排除プロトコル（たとえば、Dijkstraのバイナリセマフォの抽象化版であるQlock）を例に用い事例研究を行った。相互排除プロトコルの満たすべき性質のひとつは無排斥性（プロセスがきわどい領域に入りたい場合、いつでもそのうち必ず入ることができる）であり、Leads-to性質で表現することができる。MaudeのLTLモデル検査器のみでは遂行不可能なモデル検査を、「状態空間を２つのレイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法」で可能になることを示すことができた。
（２）当該年度には予定していなかった研究成果発表を達成した：
研究成果発表：研究成果を、ミャンマー・ヤンゴンで開催された国際会議ICAIT2019等で発表した。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
予定していた研究実施計画を予定どおりに実施できたことに加え、予定していなかった研究成果発表を国際会議論文（IEEEで出版）として達成したためである。
|
| Strategy for Future Research Activity |
まずは以下の令和2年度の研究実施計画に則り本研究課題を推進する：
理論研究：pとqを状態命題としたとき、状態空間に対してのp |-> qのモデル検査と等価となる、状態空間を２以上（L+1、ここでLは正整数） のレイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法を考案する。等価性の証明を行う。アルゴリズムの考案：理論研究で得られる「状態空間をL+1レイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法」に基づきアルゴリズムを設計する。支援ツールの開発：そのアルゴリズムを実現するツールを開発する。開発は、書換え論理に基づく計算機言語であるMaudeを使う予定である。モデル検査の対象となるシステムの仕様もMaudeで作成する。事例研究：相互排除プロトコル（たとえば、Dijkstraのバイナリセマフォの抽象化版であるQlock）を例に用い事例研究を行う。相互排除プロトコルの満たすべき性質のひとつは無排斥性（プロセスがきわどい領域に入りたい場合、いつでもそのうち必ず入ることができる）であり、Leads-to性質で表現することができる。遂行不可能なモデル検査を、「状態空間をL+1レイヤーに分割し得られる複数の小さな状態空間に対しモ デル検査を行う方法」で可能になることを示すことで提案方法の有効性を実証する。研究成果発表：国際会議（たとえば、27th Asia-Pacific Software Engineering Conference；2020年12月1日～4日にシンガポールで開催予定；CORE Rank B）や国際誌（たとえば、International Journal of Software Engineering and Knowledge Engineering；IF 0.4；CORE Rank B）に論文を投稿する。
上記計画を達成できた後に、提案方法をeventually性質などの他のLTL論理式で記述可能な性質を扱うことができるように拡張し、アルゴリズムの考案や支援ツールの開発などを実施する予定である。
|
