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

大規模・複雑なハイブリッドシステムのための区間制約プログラミング技術

研究課題

研究課題/領域番号 18K11240
研究種目

基盤研究(C)

配分区分基金
応募区分一般
審査区分 小区分60050:ソフトウェア関連
研究機関北陸先端科学技術大学院大学 (2019-2022)
福井大学 (2018)

研究代表者

石井 大輔  北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)

研究期間 (年度) 2018-04-01 – 2023-03-31
研究課題ステータス 完了 (2022年度)
配分額 *注記
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2021年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2020年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2019年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2018年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
キーワードハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム
研究成果の概要

連続離散ハイブリッドシステム(HS)のための制約プログラミング技術を開発することを目指し,大規模・複雑な組込みシステムをモデリングしたHSに対し,高信頼かつ有用な解析を実施する手法・ツールに関する研究を実施した.制約プログラミング技術に基づき,安全性のモデル検査や目的関数の最適化をする手法・ツールを提案した.提案手法は,SimulinkおよびAcumenで記述したHSを,実数,浮動小数点数,区間等の領域の変数をもつ制約へと符号化し,ソルバーによる解析を行う.産業界由来のモデルによる実験により,提案手法の性能と有用性を確認するとともに,基本手法・実装については正しさの形式的検証を実施した.

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

学術的意義として,一般的には扱うのが難しい大規模複雑なハイブリッドシステムを解析する手法の開発に取り組み,その効果を示す実験結果を得たことが挙げられる.有用な実例を検査するため,制約への符号化法,部品や繰り返しを考慮した検査法,モンテカルロ法との連携,大規模並列化,提案手法の実装技術等,複数の面について研究した.また,手法・実装自体の検証に取り組み,形式手法の研究過程の機械化・高信頼化を進めた意義がある.
社会的意義として,提案手法を実世界で稼働するシステムに対して適用し,そのモデルの安全性検査等に役立てられることが挙げられる.

報告書

(6件)
  • 2022 実績報告書   研究成果報告書 ( PDF )
  • 2021 実施状況報告書
  • 2020 実施状況報告書
  • 2019 実施状況報告書
  • 2018 実施状況報告書
  • 研究成果

    (27件)

すべて 2023 2022 2020 2019 2018 その他

すべて 国際共同研究 (1件) 雑誌論文 (5件) (うち国際共著 2件、 査読あり 5件、 オープンアクセス 1件) 学会発表 (17件) (うち国際学会 4件、 招待講演 1件) 備考 (4件)

  • [国際共同研究] PTIT/VNU University of Science, Hanoi(ベトナム)

    • 関連する報告書
      2022 実績報告書
  • [雑誌論文] Coverage Testing of Industrial Simulink Models Using Monte-Carlo and SMT-Based Methods2023

    • 著者名/発表者名
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
    • 雑誌名

      Proc. 22nd International Conference on Software Quality, Reliability and Security (QRS)

      巻: - ページ: 422-433

    • DOI

      10.1109/qrs57517.2022.00050

    • 関連する報告書
      2022 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] Approximate Translation from Floating-Point to Real-Interval Arithmetic2022

    • 著者名/発表者名
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
    • 雑誌名

      Proc. NASA Formal Methods

      巻: 13260 ページ: 733-751

    • DOI

      10.1007/978-3-031-06773-0_39

    • ISBN
      9783031067723, 9783031067730
    • 関連する報告書
      2022 実績報告書
    • 査読あり
  • [雑誌論文] SMT-Based Model Checking of Industrial Simulink Models2022

    • 著者名/発表者名
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
    • 雑誌名

      Proc. 23rd International Conference on Formal Engineering Methods (ICFEM)

      巻: 13478 ページ: 156-172

    • DOI

      10.1007/978-3-031-17244-1_10

    • ISBN
      9783031172434, 9783031172441
    • 関連する報告書
      2022 実績報告書
    • 査読あり / 国際共著
  • [雑誌論文] Template-Based Monte-Carlo Test-Suite Generation for Large and Complex Simulink Models2020

    • 著者名/発表者名
      Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
    • 雑誌名

      IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

      巻: E103.A 号: 2 ページ: 451-461

    • DOI

      10.1587/transfun.2019MAP0010

    • NAID

      130007793381

    • ISSN
      0916-8508, 1745-1337
    • 年月日
      2020-02-01
    • 関連する報告書
      2019 実施状況報告書
    • 査読あり / オープンアクセス
  • [雑誌論文] Computer-assisted verification of four interval arithmetic operators2020

    • 著者名/発表者名
      Daisuke Ishii, Tomohito Yabu
    • 雑誌名

      Journal of Computational and Applied Mathematics

      巻: 377 ページ: 1-13

    • 関連する報告書
      2020 実施状況報告書 2019 実施状況報告書
    • 査読あり
  • [学会発表] Approximate Translation from Floating-Point to Real-Interval Arithmetic2022

    • 著者名/発表者名
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
    • 学会等名
      NASA Formal Methods
    • 関連する報告書
      2021 実施状況報告書
    • 国際学会
  • [学会発表] Formalizing the Soundness of the Encoding Methods of SAT-based Model Checking2020

    • 著者名/発表者名
      Daisuke Ishii, Saito Fujii
    • 学会等名
      International Symposium on Theoretical Aspects of Software Engineering (TASE)
    • 関連する報告書
      2020 実施状況報告書 2019 実施状況報告書
    • 国際学会
  • [学会発表] SMTソルバを用いたSimulinkモデルのテストケース生成2020

    • 著者名/発表者名
      八田 竜起,石井 大輔
    • 学会等名
      情報処理学会全国大会
    • 関連する報告書
      2019 実施状況報告書
  • [学会発表] 区間制約ソルバにおけるパラメータ化制約の導入2020

    • 著者名/発表者名
      野村 亮太, 石井 大輔
    • 学会等名
      情報処理学会全国大会
    • 関連する報告書
      2019 実施状況報告書
  • [学会発表] A scalable Monte-Carlo test-case generation tool for large and complex simulink models2019

    • 著者名/発表者名
      Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
    • 学会等名
      International Workshop on Modelling in Software Engineerings (MiSE)
    • 関連する報告書
      2019 実施状況報告書
    • 国際学会
  • [学会発表] Why3を用いた区間べき関数のプログラム検証2019

    • 著者名/発表者名
      村上 涼星, 薮 智仁, 石井 大輔
    • 学会等名
      日本ソフトウェア科学会第36回大会
    • 関連する報告書
      2019 実施状況報告書
  • [学会発表] Acumen を用いたハイブリッドシステムの統計的モデル検査2019

    • 著者名/発表者名
      井上晃輔, 石井大輔
    • 学会等名
      電子情報通信学会ソフトウェアサイエンス研究会
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] Simulink モデルの SMT-LIB エンコード方法に関する実験2019

    • 著者名/発表者名
      武仲紘輝, 石井大輔
    • 学会等名
      電子情報通信学会システム数理と応用研究会
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] Duracz らの操作的意味論に基づく ハイブリッドシステムの高信頼シミュレータの実装2019

    • 著者名/発表者名
      小嶋翔太, 石井大輔
    • 学会等名
      電子情報通信学会システム数理と応用研究会
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] 証明支援系 Coq を用いた 有界モデル検査アルゴリズムの検証2019

    • 著者名/発表者名
      藤井采人, 石井大輔
    • 学会等名
      情報処理学会プログラミング研究会
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] 区間解析法とモンテカルロ法の連携による Simulink テストケースの自動生成2018

    • 著者名/発表者名
      石井大輔, 野村亮太, 八田竜起, 冨田 尭, 青木利晃
    • 学会等名
      日本ソフトウェア科学会第35回大会
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] 大規模複雑 Simulink モデルのための Monte-Carlo 最適化に基づいたテスト自動生成ツール2018

    • 著者名/発表者名
      冨田 尭, 石井大輔, 村上 徹, 竹内成樹, 青木利晃
    • 学会等名
      組込みシステムシンポジウム
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] Machine-Aided Verification of Four Interval Arithmetic Operators2018

    • 著者名/発表者名
      Tomohito Yabu, Daisuke Ishii
    • 学会等名
      International Symposium on Scientific Computing, Computer Arithmetic, and Verified Numerical Computations (SCAN)
    • 関連する報告書
      2018 実施状況報告書
    • 国際学会
  • [学会発表] Why3を用いた区間演算ライブラリの検証2018

    • 著者名/発表者名
      石井大輔, 藪 智仁
    • 学会等名
      第2回 精度保証付き数値計算の実問題への応用研究集会
    • 関連する報告書
      2018 実施状況報告書
    • 招待講演
  • [学会発表] 証明支援系 Coq を用いた有界モデル検査アルゴリズムの検証2018

    • 著者名/発表者名
      藤井采人, 石井大輔
    • 学会等名
      第16回ディペンダブルシステムワークショップ
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] Why3 を用いた区間演算プログラムの検証2018

    • 著者名/発表者名
      藪 智仁, 石井大輔
    • 学会等名
      第16回ディペンダブルシステムワークショップ
    • 関連する報告書
      2018 実施状況報告書
  • [学会発表] スケーラブルな並列探索による最適化問題の求解2018

    • 著者名/発表者名
      泉 翔太, 石井大輔, 美添一樹
    • 学会等名
      第167回HPC研究会
    • 関連する報告書
      2018 実施状況報告書
  • [備考] Artifact for NFM'22 Submission

    • URL

      https://zenodo.org/record/6387089#.ZC6eQRVBwqs

    • 関連する報告書
      2022 実績報告書
  • [備考] PROMPT

    • URL

      https://www.gaio.co.jp/products/prompt-2/

    • 関連する報告書
      2022 実績報告書
  • [備考] Encoded results of Simulink models in SMT-LIB

    • URL

      https://zenodo.org/record/6781295#.ZC6hrRVBwqs

    • 関連する報告書
      2022 実績報告書
  • [備考] SAT-based Model Checking in Coq

    • URL

      https://github.com/dsksh/coq-smc

    • 関連する報告書
      2019 実施状況報告書

URL: 

公開日: 2018-04-23   更新日: 2024-01-30  

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

Powered by NII kakenhi