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

元可扩展定理证明器和并行模型检查器融合，实现大规模快速形式验证

• 批准号: 19K11821
• 负责人: Wasaki Katsumi
• 金额: $ 2.83万
• 依托单位: Shinshu University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2019
• 资助国家: 日本
• 起止时间: 2019-04-01 至 2023-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19K11821/
• 关键词: 非同期並列システム; ハードウェアコンパイラ; 定理証明器; モデル検査器; 形式検証系; 関数型言語系; 状態空間生成; ペトリネット; 形式検証; モデル検査

项目成果

An Approach for Flow Net Subgraph to Modelling and Analysis of Flexible Manufacturing Systems

柔性制造系统流网子图建模与分析方法

• 发表时间: 2020
• 作者: Yojiro HARIE;Katsumi WASAKI
• 通讯作者: Katsumi WASAKI

サブマーキング法を用いたペトリネット状態空間の抽象化と準ホーム状態

使用子标记方法抽象Petri网状态空间和准主状态

• 发表时间: 2021
• 作者: Daichi YAMAMICHI;Seigo SHIGENAKA;Kazuhisa NAKASHO;Katsumi WASAKI;三浦朋己，和﨑克己
• 通讯作者: 三浦朋己，和﨑克己

Analysis of the Structural Liveness and Boundedness in Weighted Free-Choice Net based on Circuit Flow Values

基于电路流值的加权自由选择网络的结构活性和有界性分析

• 发表时间: 2020
• 作者: Yojiro HARIE;Katsumi WASAKI
• 通讯作者: Katsumi WASAKI

可達判定条件が既知であるサブクラス定義に反する閉路検知機能を有するペトリネット解析ツールの開発

开发 Petri 网分析工具，该工具具有检测违反已知可达性标准的子类定义的循环的功能

• 发表时间: 2020
• 作者: Yojiro HARIE;Katsumi WASAKI;南 史弥，和﨑克己;渡貫正也，和﨑克己
• 通讯作者: 渡貫正也，和﨑克己

Description and Verification of Systolic Array Parallel Computation Model in Synchronous Circuit using LOTOS

LOTOS同步电路脉动阵列并行计算模型的描述与验证

• 发表时间: 2023
• 期刊: Proceedings of 20th International Conference on Information Technology-New Generations (ITNG 2023), Advances in Intelligent Systems and Computing, Springer
• 作者: Yuya CHIBA;Katsumi WASAKI
• 通讯作者: Katsumi WASAKI