連続・離散ハイブリッド領域のための区間制約プログラミング技術

• 研究課題/領域番号: 15K15968
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: ソフトウェア
• 研究機関: 福井大学
• 研究代表者: 石井 大輔 福井大学, 学術研究院工学系部門, 講師 (00454025)
• 研究協力者: 上田 和紀 ; GOLDSZTEJN Alexandre ; 中島 震 ; 細部 博史 ; 美添 一樹 ; 渡部 卓雄
• 研究期間 (年度): 2015-04-01 – 2018-03-31
• 研究課題ステータス: 完了 (2017年度)
• 配分額: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円); 2017年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2016年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2015年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
• キーワード: ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム / 区間制約

研究成果の概要

連続的または離散的な振る舞いをするハイブリッドシステムを区間制約プログラミングのアプローチで記述・求解するとともに，さまざまな解析を高信頼に実施する技術を設計・実装した．解析では，実数計算の精度保証，関数集合を記述した微分方程式，時間軸上の性質を記述した時相論理式等を扱うが，提案手法はこれらを制約プログラミングの枠組みでとらえる点を特徴とする．実装にあたっては，一部を検証済みコードとして信頼性を高めるとともに，求解処理を並列化してスパコンを利用した効率化をはかった．ハイブリッドシステムの例を基本的なものから産業界由来のものまで収集し，提案手法の有効性を実験により評価した．

研究成果

• [国際共同研究] CNRS(フランス)
• [国際共同研究] Halmstad大学(スウェーデン)
• [国際共同研究] CNRS(フランス)
• [国際共同研究] Halmstad大学(スウェーデン)
• [国際共同研究] CNRS(フランス)
• [雑誌論文] HySIA: Tool for Simulating and Monitoring Hybrid Automata Based on Interval Analysis (2017)
  • 著者名/発表者名: Daisuke Ishii, Alexandre Goldsztejn
  • 雑誌名: Proceedings of International Conference on Runtime Verification, Lecture Notes in Computer Science 巻: 10548 ページ: 370-379
  • DOI: 10.1007/978-3-319-67531-2_23
  • ISBN: 9783319675305, 9783319675312
  • 査読あり / 国際共著
• [雑誌論文] A Parallelotope Method for Hybrid System Simulation (2016)
  • 著者名/発表者名: A. Goldsztejn, D. Ishii
  • 雑誌名: Reliable Computing 巻: 23 ページ: 163-185
  • 査読あり / オープンアクセス / 国際共著 / 謝辞記載あり
• [雑誌論文] Monitoring Temporal Properties Using Interval Analysis (2016)
  • 著者名/発表者名: D. Ishii, N. Yonezaki, A. Goldsztejn
  • 雑誌名: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences 巻: E99.A 号: 2 ページ: 442-453
  • DOI: 10.1587/transfun.E99.A.442
  • NAID: 130005121531
  • ISSN: 0916-8508, 1745-1337
  • 査読あり / 国際共著 / 謝辞記載あり
• [学会発表] An Extended GLB Library for Optimization Problems (2018)
  • 著者名/発表者名: Shota Izumi, Daisuke Ishii, Kazuki Yoshizoe
  • 学会等名: HPC Asia
  • 国際学会
• [学会発表] Reliable Simulation and Monitoring of Hybrid Systems Based on Interval Analysis (2017)
  • 著者名/発表者名: Daisuke Ishii, Alexandre Goldsztejn, Naoki Yonezaki
  • 学会等名: CyPhy Workshop
  • 国際学会 / 招待講演
• [学会発表] Template-Based Monte-Carlo Test Generation for Simulink Models (2017)
  • 著者名/発表者名: T. Tomita, D. Ishii, T. Murakami, S. Takeuchi, T. Aoki
  • 学会等名: CyPhy Workshop
  • 国際学会
• [学会発表] ハイブリッドシステムの可到達集合の精度保証 (2017)
  • 著者名/発表者名: 石井大輔
  • 学会等名: 第1回 精度保証付き数値計算の実問題への応用研究集会 (NVR)
  • 招待講演
• [学会発表] Acumen を用いたサイバーフィジカルシステムの統計的モデル検査 (2017)
  • 著者名/発表者名: 井上晃輔, 石井大輔
  • 学会等名: 第15回 ディペンダブルシステムワークショップ (DSW)
• [学会発表] Why3 を用いた区間演算ライブラリの検証 (2017)
  • 著者名/発表者名: 薮 智仁, 石井大輔
  • 学会等名: 日本ソフトウェア科学会第34回大会
• [学会発表] 証明支援系 Coq を用いた有界モデル検査 (2017)
  • 著者名/発表者名: 藤井采人, 石井大輔
  • 学会等名: 日本ソフトウェア科学会第34回大会
• [学会発表] X10 GLB ライブラリの最適化問題のための拡張 (2017)
  • 著者名/発表者名: 泉 翔太, 石井大輔, 美添一樹
  • 学会等名: 電気関係学会北陸支部連合大会
• [学会発表] 並列 RCSP ソルバーの求解過程の可視化 (2017)
  • 著者名/発表者名: 香椎蓮司, 石井大輔
  • 学会等名: 電気関係学会北陸支部連合大会
• [学会発表] ハイブリッドシステムの統計的モデル検査 (2016)
  • 著者名/発表者名: 石井大輔, 冨田 尭, 米崎直樹
  • 学会等名: 信学会総合大会
  • 発表場所: 福岡県福岡市
  • 年月日: 2016-03-16
  • 招待講演
• [学会発表] 時相論理式の反証を用いた制御器のチューニング (2016)
  • 著者名/発表者名: 峰尾太陽, 石井大輔, 渡部卓雄
  • 学会等名: 電子情報通信学会MSS研究会
  • 発表場所: 山口県下関市
  • 年月日: 2016-03-04
• [学会発表] 区間解析による時相論理式の頑健性モニタリング (2016)
  • 著者名/発表者名: 石井大輔
  • 学会等名: 電子情報通信学会MSS研究会
  • 発表場所: 石川県金沢市
  • 年月日: 2016-01-25
  • 招待講演
• [学会発表] 区間解析に基づく非線形ハイブリッドオートマトンのシミュレーション・検証ツール (2016)
  • 著者名/発表者名: 石井大輔
  • 学会等名: 第14回ディペンダブルシステムワークショップ
  • 発表場所: 北海道函館市
• [学会発表] Simulinkモデルに対するテストスイート自動生成 (2016)
  • 著者名/発表者名: 冨田尭, 石井大輔, 青木利晃
  • 学会等名: 第14回ディペンダブルシステムワークショップ
  • 発表場所: 北海道函館市
• [学会発表] 数値制約ソルバーのスケーラブルな並列化 (2015)
  • 著者名/発表者名: 石井大輔, 美添一樹, 鈴村豊太郎
  • 学会等名: 日本ソフトウェア科学会第32回大会
  • 発表場所: 東京都新宿区
  • 年月日: 2015-09-09
• [学会発表] Scalable Parallel Numerical Constraint Solver Using Global Load Balancing (2015)
  • 著者名/発表者名: D. Ishii, K. Yoshizoe, T. Suzumura
  • 学会等名: ACM SIGPLAN Workshop on X10
  • 発表場所: 米国ポートランド
  • 年月日: 2015-06-14
  • 国際学会
• [学会発表] Monitoring Bounded LTL Properties Using Interval Analysis (2015)
  • 著者名/発表者名: D. Ishii, N. Yonezaki, A. Goldsztejn
  • 学会等名: 8th International Workshop on Numerical Software Verification (NSV)
  • 発表場所: 米国シアトル
  • 年月日: 2015-04-13
  • 国際学会
• [備考] HySIA GitHub
  • URL: https://github.com/dsksh/hysia