• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2022 Fiscal Year Annual Research Report

A divide and conquer approach to parallelization of LTL model checking

Research Project

Project/Area Number 19H04082
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

緒方 和博  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)

Project Period (FY) 2019-04-01 – 2023-03-31
Keywordsモデル検査 / 分割統治 / 並列化 / leads-to性 / eventual性 / 条件付安定性 / until性 / until安定性
Outline of Annual Research Achievements

線形時相論理(LTL)で表現可能な代表的な性質のクラス(lead-to性、eventual性、条件付安定性、until性、until安定性)に対し、各初期状態から構築される無限木を複数の層に分割し、複数の部分空間ごとに独立にモデル検査することでもとの状態空間に対するモデル検査と同等のモデル検査結果を得ることのできる技術を考案すると共に正当性を証明した。部分空間ごとに独立に行えるモデル検査を同時に行うことで並列モデル検査を可能とする。モデル検査におけるもっともやっかいな状態空間爆発を緩和可能であると共にモデル検査にとって重要な実行速度の改善に貢献することができる。until性とuntil安定性を除き、逐次版と並列版の支援ツールを作成した。支援ツールの作成にはMaudeを用いた。支援ツールの実装において、部分空間のモデル検査においてすべての反例をひとつずつ探すことが実行面におけるボトルネックになっていたため、Tarjanの提案した、強連結要素を探すアルゴリズム用いて一度にすべての反例を探すことの出来るモデル検査器を、MaudeのLTLモデル検査器で使われているソフトウェアコンポネントを再利用するとで作成し、支援ツールで利用することにした。これによりそのボトルネックを解消することができた。提案方法では、上述した無限木をどのような層に分割するのか(レイヤーコンフィグレーション)がモデル検査の性能に大きく影響する。そこで、より良いレイヤーコンフィグレーションを探すことを支援するツールを作成した。事例実験により効果を確認することができた。提案方法は、LTLモデル検査の並列化のみならず、セキュリティプロトコル専用の解析ツールであるMaude-NPAやJavaのモデル検査器であるJava Pathfinder(JPF)の並列化にも有効であることを示した。

Research Progress Status

令和4年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

令和4年度が最終年度であるため、記入しない。

  • Research Products

    (6 results)

All 2022

All Journal Article (4 results) (of which Peer Reviewed: 4 results,  Open Access: 3 results) Presentation (2 results) (of which Int'l Joint Research: 2 results)

  • [Journal Article] Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way2022

    • Author(s)
      Canh Minh Do、Phyo Yati、Ogata Kazuhiro
    • Journal Title

      IEEE Access

      Volume: 10 Pages: 133749~133765

    • DOI

      10.1109/ACCESS.2022.3230844

    • Peer Reviewed / Open Access
  • [Journal Article] Parallel Specification-Based Testing for Concurrent Programs2022

    • Author(s)
      Canh Minh Do、Ogata Kazuhiro
    • Journal Title

      IEEE Access

      Volume: 10 Pages: 24955~24975

    • DOI

      10.1109/ACCESS.2022.3155629

    • Peer Reviewed / Open Access
  • [Journal Article] Parallel Maude-NPA for Cryptographic Protocol Analysis2022

    • Author(s)
      Canh Minh Do、Riesco Adrian、Escobar Santiago、Ogata Kazuhiro
    • Journal Title

      14th International Workshop on Rewriting Logic and Its Applications

      Volume: LNCS 13252 Pages: 253~273

    • DOI

      10.1007/978-3-031-12441-9_13

    • Peer Reviewed
  • [Journal Article] A divide and conquer approach to until and until stable model checking2022

    • Author(s)
      Canh Minh Do、Phyo Yati、Ogata Kazuhiro
    • Journal Title

      34th International Conference on Software Engineering and Knowledge Engineering

      Volume: NA Pages: 388~393

    • DOI

      10.18293/SEKE2022-058

    • Peer Reviewed / Open Access
  • [Presentation] Parallel Maude-NPA for Cryptographic Protocol Analysis2022

    • Author(s)
      Canh Minh Do
    • Organizer
      14th International Workshop on Rewriting Logic and Its Applications
    • Int'l Joint Research
  • [Presentation] A divide and conquer approach to until and until stable model checking2022

    • Author(s)
      Canh Minh Do
    • Organizer
      34th International Conference on Software Engineering and Knowledge Engineering
    • Int'l Joint Research

URL: 

Published: 2023-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi