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

2021 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モデル検査 / 状態空間爆発 / 分割統治 / 線形時相論理 / Maude
Outline of Annual Research Achievements

(1)当該年度に予定していた研究実施計画に則り研究を実施し、以下の実績を達成した:
理論研究:pとqを状態命題としたとき、状態空間に対する<> p(Eventual性質)とp |-> [] q(Conditional stable性質)のモデル検査と等価となる状態空間を2以上(L+1、ここでLは正整数)のレイヤーに分割し得られる複数の小さな状態空間に対するモデル検査を行う方法を考案すると共に等価性の証明を行った。アルゴリズムの考案:理論研究で得られる「状態空間をL+1レイヤーに分割し得られる複数の小さな状態空間に対しモデル検査を行う方法」に基づきアルゴリズムを設計した。支援ツールの開発:そのアルゴリズムを実現する支援ツールの逐次版と並列版のプロトタイプをMaudeを実装言語として用いて作成した。前年度に作成したLeads-to性質用の支援ツール(逐次版と並列版)のプロトタイプを基に完成版を開発した。事例研究:既存のLTLモデル検査器では状態爆発のためモデル検査不能になる事例を支援ツールの逐次版を用いることでモデル検査可能になること、支援ツールの並列版を用いることでモデル検査の実行速度が改善できることを確認した。研究成果発表:成果を複数の国際会議で発表すると共に国際会議論文を出版した。
(2)当該年度には予定していなかった研究成果を達成した:
本研究で提案する方法は、ソフトウェアの設計のためのモデル検査用であった。プログラムを対象とするソフトウェアモデル検査器である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

理論研究:状態空間を2以上(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などの相互排除プロトコルを事例として用い、提案方法・支援ツールの有効性を示す事例研究を行う。研究成果発表:国際会議や国際誌に論文を投稿する。

  • Research Products

    (8 results)

All 2022 2021 Other

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

  • [Int'l Joint Research] Universidad Complutense de Madrid(スペイン)

    • Country Name
      SPAIN
    • Counterpart Institution
      Universidad Complutense de Madrid
  • [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] A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties2021

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

      7th International Symposium on System and Software Reliability

      Volume: 0 Pages: 155~166

    • DOI

      10.1109/ISSSR53171.2021.00011

    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] A Divide & Conquer Approach to Conditional Stable Model Checking2021

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

      18th International Colloquium on Theoretical Aspects of Computing

      Volume: 0 Pages: 105~111

    • DOI

      10.1007/978-3-030-85315-0_7

    • Peer Reviewed
  • [Journal Article] A support tool for the L + 1-layer divide & conquer approach to leads-to model checking2021

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

      45th IEEE Computer Society Computers, Software, and Applications Conference

      Volume: 0 Pages: 854~863

    • DOI

      10.1109/COMPSAC51774.2021.00118

    • Peer Reviewed
  • [Presentation] A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties2021

    • Author(s)
      Do Canh Minh
    • Organizer
      7th International Symposium on System and Software Reliability
    • Int'l Joint Research
  • [Presentation] A Divide & Conquer Approach to Conditional Stable Model Checking2021

    • Author(s)
      Phyo Yati
    • Organizer
      18th International Colloquium on Theoretical Aspects of Computing
    • Int'l Joint Research
  • [Presentation] A support tool for the L + 1-layer divide & conquer approach to leads-to model checking2021

    • Author(s)
      Phyo Yati
    • Organizer
      45th IEEE Computer Society Computers, Software, and Applications Conference
    • Int'l Joint Research

URL: 

Published: 2022-12-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi