• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2023 年度 研究成果報告書

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

研究課題

  • PDF
研究課題/領域番号 19H04084
研究種目

基盤研究(B)

配分区分補助金
応募区分一般
審査区分 小区分60050:ソフトウェア関連
研究機関京都大学

研究代表者

末永 幸平  京都大学, 情報学研究科, 准教授 (70633692)

研究分担者 五十嵐 淳  京都大学, 情報学研究科, 教授 (40323456)
海野 広志  筑波大学, システム情報系, 准教授 (80569575)
池渕 未来  京都大学, 情報学研究科, 助教 (70961796)
研究期間 (年度) 2019-04-01 – 2024-03-31
キーワードハイブリッドシステム / モデル検査 / プログラム検証 / 形式検証 / ブラックボックス検査 / モニタリング / PDR
研究成果の概要

IoT システムの数学的なモデルであるハイブリッドシステムのための形式検証手法を主眼において研究した.主な研究成果としては (1) ハイブリッドシステム検証のための PDR モデル検査アルゴリズムの拡張,(2) 束論を用いた PDR の本質の解明が得られた.この他にも,IoT システムに関わるソフトウェアの主要な実装言語であるポインタを含む命令型言語のための型理論に基づく検証手法や,ブラックボックスを含むシステムを効率的にテストする手法,機微情報を含むデータを暗号文のままでモニタリング可能とする秘匿モニタリング手法等の成果が得られた.

自由記述の分野

形式検証

研究成果の学術的意義や社会的意義

この研究課題では,IoTシステムの安全性を確保するための新しい形式検証手法について扱った.特に,ソフトウェアと物理的プロセスが融合したハイブリッドシステムの安全性を保証するために,PDR (Property-Directed Reachability) と呼ばれるモデル検査手法を拡張した.この技術により,IoTデバイスが互いに安全に連携し,データを交換できるようになる.この成果は,社会全体のIoT技術の信頼性と効率を向上させ,高度なデジタル化社会の発展に大きく貢献する成果である.

URL: 

公開日: 2025-01-30  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi