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

A divide and conquer approach to parallelization of LTL model checking

Research Project

Project/Area Number 19H04082
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Review Section Basic Section 60050:Software-related
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

OGATA Kazuhiro  北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)

Project Period (FY) 2019-04-01 – 2023-03-31
Project Status Completed (Fiscal Year 2022)
Budget Amount *help
¥16,770,000 (Direct Cost: ¥12,900,000、Indirect Cost: ¥3,870,000)
Fiscal Year 2022: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2021: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2020: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2019: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Keywordsモデル検査 / 分割統治 / 並列化 / leads-to性 / eventual性 / 条件付安定性 / until性 / until安定性 / 状態空間爆発 / 線形時相論理 / Maude / 状態爆発 / LTL / Leads-to性質 / 状態機械
Outline of Research at the Start

我々の生活を便利にするシステムは高信頼であるべきだ。さもなければ、多額の財産を失う等の多大な不便をこうむることになる。システムを高信頼にするために使うことのできる技術のひとつはモデル検査である。システムが期待される要件を満たすかどうかを自動で検証出来る。しかし、システムの到達可能状態空間が大きくなり過ぎてモデル検査不能になる問題が起こる。本研究計画では、到達可能状態空間を複数の部分空間に分割し、各々の部分空間でモデル検査を行えるようにすることでこの問題を緩和することを試みる。加えて、複数の部分空間に対するモデル検査を同時並列に実行することでモデル検査の効率化も試みる。

Outline of Final Research Achievements

By splitting an infinite state tree constructed from each initial state into multiple layers and tackling each sub-state space, the state space explosion in model checking can be alleviated. By handling multiple sub-state spaces simultaneously, the model checking running performance can be improved. Several important classes of linear temporal logic (LTL) properties, such as leads-to properties, can be dealt with. We built sequential and parallel versions of a support tool for each property class and conduct cases studies with such tools, demonstrating the usefulness of the techniques proposed and the support tools.

Academic Significance and Societal Importance of the Research Achievements

ソフトウェアは我々の生活に深く入り込んでいる。大変便利であるが、複雑であればあるほど潜在的不具合が存在する可能性は大きい。顕在化すると、財政的損失ばかりでなく人命にも危険が及ぶ可能性すらある。このため、潜在的不具合は可能な限り取り除いたほうが良い。そのための有望な技術にモデル検査がある。しかし、ソフトウェア産業界において日常業務での使用に耐えうるようにするには解決すべき課題がある。状態空間爆発の緩和と実行速度の改善だ。状態空間を複数の空間に分割することで状態空間爆発を緩和し、複数の部分状態空間を並列にモデル検査することで実行速度を改善した。ソフトウェア産業界での実用化に向けて前進できた。

Report

(5 results)
  • 2022 Annual Research Report   Final Research Report ( PDF )
  • 2021 Annual Research Report
  • 2020 Annual Research Report
  • 2019 Annual Research Report
  • Research Products

    (27 results)

All 2022 2021 2020 2019 Other

All Int'l Joint Research (1 results) Journal Article (15 results) (of which Int'l Joint Research: 2 results,  Peer Reviewed: 15 results,  Open Access: 6 results) Presentation (11 results) (of which Int'l Joint Research: 11 results,  Invited: 1 results)

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

    • Related Report
      2021 Annual Research Report
  • [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

    • Related Report
      2022 Annual Research Report
    • 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

    • Related Report
      2022 Annual Research Report 2021 Annual Research Report
    • 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

    • ISBN
      9783031124402, 9783031124419
    • Related Report
      2022 Annual Research Report
    • 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

    • Related Report
      2022 Annual Research Report
    • 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

    • Related Report
      2021 Annual Research Report
    • 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

    • ISBN
      9783030853143, 9783030853150
    • Related Report
      2021 Annual Research Report
    • 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

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A Divide & Conquer Approach to Leads-to Model Checking2021

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

      The Computer Journal

      Volume: - Issue: 6 Pages: 1353-1364

    • DOI

      10.1093/comjnl/bxaa183

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] A Divide and Conquer Approach to Eventual Model Checking2021

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

      Mathematics

      Volume: 9 Issue: 4 Pages: 368-368

    • DOI

      10.3390/math9040368

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] A Generic Approach on How to Formally Specify and Model Check Path Finding Algorithms: Dijkstra, A* and LPA*2020

    • Author(s)
      Ogata Kazuhiro
    • Journal Title

      International Journal of Software Engineering and Knowledge Engineering

      Volume: 30 Issue: 10 Pages: 1481-1523

    • DOI

      10.1142/s0218194020400215

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A divide & conquer approach to testing concurrent programs with JPF2020

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

      27th Asia-Pacific Software Engineering Conference (27th APSEC)

      Volume: - Pages: 356-364

    • DOI

      10.1109/apsec51365.2020.00044

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Parallel stratified random testing for concurrent programs2020

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

      IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C)

      Volume: - Pages: 79-86

    • DOI

      10.1109/qrs-c51114.2020.00024

    • Related Report
      2020 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and?Maude2020

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

      Proc. of 9th International Workshop on SOFL+MSVL

      Volume: - Pages: 42-58

    • DOI

      10.1007/978-3-030-41418-4_4

    • ISBN
      9783030414177, 9783030414184
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Toward development of a tool supporting a 2-layer divide & conquer approach to leads-to model checking2019

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

      Proc. of 2019 International Conference on Advanced Information Technologies

      Volume: - Pages: 250-255

    • DOI

      10.1109/aitc.2019.8920978

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S)2019

    • Author(s)
      Aung Moe Nandi、Phyo Yati、Ogata Kazuhiro
    • Journal Title

      Proc. of 31st International Conference on Software Engineering and Knowledge Engineerin

      Volume: - Pages: 159-164

    • DOI

      10.18293/seke2019-021

    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Presentation] Parallel Maude-NPA for Cryptographic Protocol Analysis2022

    • Author(s)
      Canh Minh Do
    • Organizer
      14th International Workshop on Rewriting Logic and Its Applications
    • Related Report
      2022 Annual Research Report
    • 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
    • Related Report
      2022 Annual Research Report
    • Int'l Joint Research
  • [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
    • Related Report
      2021 Annual Research Report
    • 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
    • Related Report
      2021 Annual Research Report
    • 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
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] A divide & conquer approach to testing concurrent programs with JPF2020

    • Author(s)
      Do Canh Minh
    • Organizer
      27th Asia-Pacific Software Engineering Conference (27th APSEC)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Parallel stratified random testingfor concurrent programs2020

    • Author(s)
      Do Canh Minh
    • Organizer
      IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] A stratified way to mitigate the state space explosion in model checking2020

    • Author(s)
      Kazuhiro Ogata
    • Organizer
      The 12th IEEE International Conference on KNOWLEDGE AND SYSTEMS ENGINEERING (KSE 2020)
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research / Invited
  • [Presentation] Toward development of a tool supporting a 2-layer divide & conquer approach to leads-to model checking2019

    • Author(s)
      Phyo Yati
    • Organizer
      2019 International Conference on Advanced Information Technologies
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and?Maude2019

    • Author(s)
      Minh Do Canh
    • Organizer
      9th International Workshop on SOFL+MSVL
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S)2019

    • Author(s)
      Phyo Yati
    • Organizer
      31st International Conference on Software Engineering and Knowledge Engineerin
    • Related Report
      2019 Annual Research Report
    • Int'l Joint Research

URL: 

Published: 2019-04-18   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi