课题基金 / 基金详情

IoT システムのための形式検証手法の深化

IoT システムのための形式検証手法の深化
深化物联网系统的形式化验证方法
批准号：
19H04084
负责人：
末永 幸平
金额：
$10.9万
依托单位：
Kyoto University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (B)
财政年份：
2019
资助国家：
日本
项目状态：
已结题
起止时间：
2019-04-01 至 2024-03-31
来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19H04084/
关键词：
プログラム検証形式検証IoTモデル検査PDR強化学習機械学習ハイブリッドシステム形式手法

项目摘要

项目成果

末永 幸平的其他基金

相似基金

相关文献

中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
本研究課題での主要なトピックの一つである仕様手動到達性 (Property Directed Reachability; PDR) を用いたモデル検査手法について，理論面で大きな成果があった．PDRは，従来、実装の詳細を伴う手続き型言語での定義が主流であり，その本質的な計算プロセスが理解しにくい状況であった．そこで我々は，束論 (Lattice Theory) を用いてPDRを理論的に再定義することで，その本質を明らかにする新しい定義を提案した．この新たな定義により，確率的システムをはじめとする様々なシステムに対する PDR が統一的に理解できることを示した．さらに，この定義に基づいた検証器を実装した．この実装は，様々なシステムの性質を差分的に実装することで，そのシステムのためのPDRを自動的に導出できるような一般的な実装となっており，その汎用性が従来実装に比して非常に高くなっている．本研究の成果を，2022年の国際会議 Computer Aided Verification (CAV) において発表した．
期刊论文(24)
专著(0)
科研奖励(0)
会议论文
Generalized Property-Directed Reachability for Hybrid Systems
DOI： 10.1007/978-3-030-39322-9_14
发表时间： 2019-10
期刊： ArXiv
影响因子： --
作者： [Kohei Suenaga;T. Ishizawa]
通讯作者： Kohei Suenaga;T. Ishizawa
ブラックボックス画像分類モデルの否定的判断根拠と色情報根拠の可視化
黑盒图像分类模型的否定判断依据和颜色信息依据可视化
DOI： --
发表时间： 2020
期刊：
影响因子： --
作者： [畠山雄気, 佐久間宏樹, 小西嘉典, 末永幸平]
通讯作者： 末永幸平
理論計算機科学事典（8.3節「型に基づくプログラム検証」）
理论计算机科学百科全书（第8.3节“基于类型的程序验证”）
DOI： --
发表时间： 2022
期刊：
影响因子： --
作者： [徳山 豪, 小林 直樹]
通讯作者： 小林 直樹
Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
Helmholtz：基于改进类型的Tezos智能合约的验证者
DOI： 10.1007/978-3-030-72013-1_14
发表时间： 2021-02-26
期刊： Tools and Algorithms for the Construction and Analysis of Systems
影响因子： --
作者： [Nishida Y, Saito H, Chen R, Kawata A, Furuse J, Suenaga K, Igarashi A]
通讯作者： Igarashi A
共 19 条
    無限小プログラミングによるハイブリッドシステムの形式検証手法
    • 批准号：
      24800035
    • 项目类别：
      Grant-in-Aid for Research Activity Start-up
    • 资助金额：
      $1.91万
    • 财政年份：
      2012
    • 负责人：
      末永 幸平
    • 依托单位：
      Kyoto University
    並行プログラムのための型理論に基づく利便性の高い静的検証手法
    • 批准号：
      11J00571
    • 项目类别：
      Grant-in-Aid for JSPS Fellows
    • 资助金额：
      $0.51万
    • 财政年份：
      2011
    • 负责人：
      末永 幸平
    • 依托单位：
      Kyoto University
    並行プログラム検証のための型システムとそのオペレーティングシステムの検証への応用
    海外基金