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

Fusion of Meta-Scalable Theorem Prover and Parallel Model Checker to Realize Large-Scale Fast Formal Verification

Research Project

Project/Area Number 19K11821
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 60010:Theory of informatics-related
Research InstitutionShinshu University

Principal Investigator

Wasaki Katsumi  信州大学, 学術研究院工学系, 教授 (70271492)

Project Period (FY) 2019-04-01 – 2023-03-31
Project Status Completed (Fiscal Year 2022)
Budget Amount *help
¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Keywords非同期並列システム / ハードウェアコンパイラ / 定理証明器 / モデル検査器 / 形式検証系 / 関数型言語系 / 状態空間生成 / ペトリネット / 形式検証 / モデル検査
Outline of Research at the Start

定理証明のプロパティ検証情報とモデル検査時の空間最適分割問題を融合し,メニーコア・クラスタ基盤上へ実装する.システム統合のため,状態空間の最適分割・合成を行うためのアルゴリズム開発と並列化ライブラリを利用したプログラム開発を行う.非同期回路や並行システムに関する形式化記述として,Mizar Mathematical Library (MML) を利用する.並列化検証システム全体の性能評価と,実システムレベルでの性能評価のために,intel Xeon Phi並列アクセラレータと,FPGA/CPLD統合設計開発ツールを使用する.

Outline of Final Research Achievements

For the purpose of rigorous property checking of circuits to be verified, a study was conducted to model the connections between logic gate elements using message-passing parallel computation. Theorem proving was done by property checking on the circuit structure and the validity of the connections. As an actual example of PE with scalable and repetitive structures, we actually wrote a theorem proof for a high radix compressor module of a high-speed multiplier circuit using multisort algebra as the theoretical basis, and performed machine verification using the Mizar proof checker. The desired properties, such as the correctness of the circuit synthesis structure and input-output relations, were successfully verified.

Academic Significance and Societal Importance of the Research Achievements

LOTOSコード生成器によって下位設計(ペトリネットモデル)が得られ、状態空間生成器を用いて初期状態から駆動するが、状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化を図るため、削除可能状態のオンライン判定アルゴリズムに関する検討を行った点に学術的意義がある。なおペトリネット検証系に関する基礎研究として、サブマーキング法を用いた状態空間の抽象化と準ホーム状態の存在検知、一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知などに関する成果を得た点についても学術的意義がある。

Report

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

    (26 results)

All 2023 2022 2021 2020 2019 Other

All Journal Article (7 results) (of which Peer Reviewed: 7 results) Presentation (18 results) (of which Int'l Joint Research: 6 results) Remarks (1 results)

  • [Journal Article] Description and Verification of Systolic Array Parallel Computation Model in Synchronous Circuit using LOTOS2023

    • Author(s)
      Yuya CHIBA, Katsumi WASAKI
    • Journal Title

      Proceedings of 20th International Conference on Information Technology-New Generations (ITNG 2023), Advances in Intelligent Systems and Computing, Springer

      Volume: 1459

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Detection of Strictly L3-Live Structures by Structural Analysis of General Petri Net Using SAT-Solver2022

    • Author(s)
      Yuta YOSHIZAWA, Katsumi WASAKI
    • Journal Title

      Proceedings of 19th International Conference on Information Technology-New Generations (ITNG 2022), Advances in Intelligent Systems and Computing, Springer

      Volume: 1421 Pages: 387-392

    • DOI

      10.1007/978-3-030-97652-1_46

    • ISBN
      9783030976514, 9783030976521
    • Related Report
      2022 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Space Abstraction and Quasi-Home States of Petri Nets Using the Submarking Method2022

    • Author(s)
      Tomoki MIURA, Katsumi WASAKI
    • Journal Title

      Proceedings of 19th International Conference on Information Technology-New Generations (ITNG 2022), Advances in Intelligent Systems and Computing, Springer

      Volume: 1421 Pages: 393-398

    • DOI

      10.1007/978-3-030-97652-1_47

    • ISBN
      9783030976514, 9783030976521
    • Related Report
      2022 Annual Research Report
    • Peer Reviewed
  • [Journal Article] An Integrated Web Platform for the Mizar Mathematical Library2022

    • Author(s)
      Hideharu FURUSHIMA, Daichi YAMAMICHI, Seigo SHIGENAKA, Kazuhisa NAKASHO, Katsumi WASAKI
    • Journal Title

      Proceedings of the 15th Conference on Intelligent Computer Mathematics (CICM 2022), LNAI

      Volume: 13467 Pages: 141-146

    • DOI

      10.1007/978-3-031-16681-5_9

    • ISBN
      9783031166808, 9783031166815
    • Related Report
      2022 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A Method for Improving Memory Efficiency of the Reachability Graph Generation Process in General Petri Nets2021

    • Author(s)
      Kohei FUJIMORI, Katsumi WASAKI
    • Journal Title

      Advances in Intelligent Systems and Computing, Springer

      Volume: 1346 Pages: 255-263

    • DOI

      10.1007/978-3-030-70416-2_33

    • NAID

      40021747769

    • ISBN
      9783030704155, 9783030704162
    • Related Report
      2021 Research-status Report
    • Peer Reviewed
  • [Journal Article] Hardware Logic Library and High-level Logic Synthesizer Combining LOTOS and A Functional Programming Language2021

    • Author(s)
      Katsumi WASAKI
    • Journal Title

      Advances in Intelligent Systems and Computing, Springer

      Volume: 1346 Pages: 313-321

    • DOI

      10.1007/978-3-030-70416-2_40

    • ISBN
      9783030704155, 9783030704162
    • Related Report
      2021 Research-status Report
    • Peer Reviewed
  • [Journal Article] Stability of the 7-3 Compressor Circuit for Wallace Tree. Part I2020

    • Author(s)
      Katsumi WASAKI
    • Journal Title

      Formalized Mathematics

      Volume: 28 Issue: 1 Pages: 65-77

    • DOI

      10.2478/forma-2020-0005

    • Related Report
      2020 Research-status Report 2019 Research-status Report
    • Peer Reviewed
  • [Presentation] グローバルクロック同期型シストリックアレイ並列モデルに対するモデル検査器を用いた多様な振る舞い解析2023

    • Author(s)
      千葉悠矢,和﨑克己
    • Organizer
      情報処理学会 第85回全国大会
    • Related Report
      2022 Annual Research Report
  • [Presentation] グローバルクロック同期型シストリックアレイ並列計算モデルのLOTOS記述と振る舞い検証2022

    • Author(s)
      千葉悠矢,和﨑克己
    • Organizer
      第21回情報科学技術フォーラム(FIT2022)
    • Related Report
      2022 Annual Research Report
  • [Presentation] ペトリネット構造解析とオカレンスネットを用いたホーム状態の判定2022

    • Author(s)
      三浦朋己,和﨑克己
    • Organizer
      第21回情報科学技術フォーラム(FIT2022)
    • Related Report
      2022 Annual Research Report
  • [Presentation] 一般ペトリネットにおける構造的性質を用いた強L2活性構造の存在性判定2022

    • Author(s)
      芳澤祐大,和﨑克己
    • Organizer
      第21回情報科学技術フォーラム(FIT2022)
    • Related Report
      2022 Annual Research Report
  • [Presentation] Mizar数学ライブラリの定理検索を行うWebアプリケーション2022

    • Author(s)
      Hideharu Furushima, Kazuhisa Nakasho and Katsumi Wasaki
    • Organizer
      第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
    • Related Report
      2021 Research-status Report
  • [Presentation] ペトリネット構造解析によるホーム状態存在性の判定2022

    • Author(s)
      三浦朋己,和﨑克己
    • Organizer
      情報処理学会 第84回全国大会
    • Related Report
      2021 Research-status Report
  • [Presentation] 一般ペトリネットの構造的性質を用いた強L3/L2活性構造の検知2022

    • Author(s)
      芳澤祐大,和﨑克己
    • Organizer
      情報処理学会 第84回全国大会 講演論文集
    • Related Report
      2021 Research-status Report
  • [Presentation] A Web Platform for Hosting the Mizar Mathematical Library2021

    • Author(s)
      Daichi YAMAMICHI, Seigo SHIGENAKA, Kazuhisa NAKASHO, Katsumi WASAKI
    • Organizer
      The 14th Conference on Intelligent Computer Mathematics (CICM 2021), Fifth Workshop on Formal Mathematics for Mathematicians (FMM2021)
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] サブマーキング法を用いたペトリネット状態空間の抽象化と準ホーム状態2021

    • Author(s)
      三浦朋己,和﨑克己
    • Organizer
      第20回情報科学技術フォーラム(FIT2021)
    • Related Report
      2021 Research-status Report
  • [Presentation] 一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知2021

    • Author(s)
      芳澤祐大,和﨑克己
    • Organizer
      第20回情報科学技術フォーラム(FIT2021)
    • Related Report
      2021 Research-status Report
  • [Presentation] Hardware Logic Library and High-level Logic Synthesizer Combining LOTOS and A Functional Programming Language2021

    • Author(s)
      Katsumi WASAKI
    • Organizer
      18th International Conference on Information Technology-New Generations (ITNG 2021)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] A Method for Improving Memory Efficiency of the Reachability Graph Generation Process in General Petri Nets2021

    • Author(s)
      Kohei FUJIMORI, Katsumi WASAKI
    • Organizer
      18th International Conference on Information Technology-New Generations (ITNG 2021)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] An Approach for Flow Net Subgraph to Modelling and Analysis of Flexible Manufacturing Systems2020

    • Author(s)
      Yojiro HARIE, Katsumi WASAKI
    • Organizer
      31st International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2020)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] Analysis of the Structural Liveness and Boundedness in Weighted Free-Choice Net based on Circuit Flow Values2020

    • Author(s)
      Yojiro HARIE, Katsumi WASAKI
    • Organizer
      2020 Computing Conference (CC2020)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] 特徴的構造を持つペトリネットにおける極小サイフォン検出アルゴリズムの動的選択2020

    • Author(s)
      南 史弥,和﨑克己
    • Organizer
      FIT2020(第19回情報科学技術フォーラム)
    • Related Report
      2020 Research-status Report
  • [Presentation] 可達判定条件が既知であるサブクラス定義に反する閉路検知機能を有するペトリネット解析ツールの開発2020

    • Author(s)
      渡貫正也,和﨑克己
    • Organizer
      FIT2020(第19回情報科学技術フォーラム)
    • Related Report
      2020 Research-status Report
  • [Presentation] An Approach for Flow Net Subgraph to Modelling and Analysis of Flexible Manufacturing Systems2020

    • Author(s)
      Yojiro Harie, Katsumi Wasaki
    • Organizer
      The 31st International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2020)
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research
  • [Presentation] フローネット変換を用いたペトリネットの構造的活性・有界性解析手法2019

    • Author(s)
      張江洋次朗,和﨑克己
    • Organizer
      電子情報通信学会 第32回 回路とシステムワークショップ(KWS32)
    • Related Report
      2019 Research-status Report
  • [Remarks] HiPS : Hierarchical Petri net Simulator

    • URL

      https://github.com/kisolab/HiPS1_released

    • Related Report
      2022 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi