信頼できるソフトウェアを実世界に組み込む

石井研究室　ISHII Laboratory
准教授：石井 大輔（ISHII Daisuke）

E-mail：
［研究分野］
ソフトウェア工学/科学、制約プログラミング
［キーワード］
組込みシステム、自律CPS、モデル検査、プログラム検証、高信頼シミュレーション

研究を始めるのに必要な知識・能力

数学の基礎知識、プログラミング能力、英語文献の読解力があるのが望ましいです。論理的な（人間同士の）対話能力と、目標達成のために地道に努力する能力を備えた学生を歓迎します。

この研究で身につく能力

セーフティクリティカルシステム（例：自律走行する車、ブロックチェーン）をモデル化・設計・実装・検証するための理論・技術を学修します。特定の理論・技術について、独自の手法を提案したり、ソフトウェアツールを実装したり、計算機上で実験したりする作業に取り組みます。その過程で、(1) 本質的な問題点をとらえて対策を打ち出す能力、(2) 研究開発コミュニティ内での位置付けや歴史を調査し、広い視野に立って研究する能力、(3) 研究成果の対外発表を通して専門内外の人々に論理的に説明する能力を身につけます。

【就職先企業・職種】 ソフトウェア産業、製造業、スタートアップ企業

研究内容

　実世界のシステムを信頼できる形で実現するため、「制約」を中間表現として扱うアプローチに取り組んでいます。アイディアや要求から具体的なシステムを開発するにあたり、(i) まず、高位モデル、論理式、数式などによるモデル化や設計をおこない、(ii) つぎに、探索による求解、数値シミュレーション、静的解析などをおこない、それらの結果を対象システムの実装・検証に利用します。また、同様のアプローチにより、データセットや制約 (ルール) に基づいた機械学習モデルを組み込んだ自律システムを扱うことを考えています。

[研究事例1] 連続・離散ハイブリッドシステムのモデリング・シミュレーション・検証

　物理系と計算機からなるシステムを直感的に記述するためのモデリング言語について研究しています。さまざまな言語 (例：ハイブリッドオートマトン、時相論理式、Simulink図) を用いて記述実験をしたり、意味論や相互の関係などを調べたりしてきました。
　記述したモデルについて、振る舞いのシミュレーションや網羅的なテスト・検証を実施することが重要です。不定値や数値誤差を区間値で包含しながら、高信頼な計算結果を求めるための手法を提案し、ツールを実装しています。

[研究事例2] 数値制約プログラミング

　実数変数をもつ制約について、探索と数値計算を用いて充足解・最適解を求める制約ソルバーの開発に取り組んできました。提案するソルバーは区間解析に基づくのが特徴で、結果について数値的な精度の保証をしたり、不定値を含んだまま求解したりすることが可能です。不定値を効率よく扱うアルゴリズムや、時間的な制約を扱う手法を提案してきました。また、ロボティクスへの応用やソルバーの並列化などにも取り組んできました。

[研究事例3] 数値計算プログラムの検証

　上記のシミュレータ、検証器、制約ソルバーの信頼性を高めることを目指し、プログラム検証に取り組んでいます。SMTソルバーや定理証明支援系を用いてその正しさを示しながら、浮動小数点数演算や煩雑な制御構造を含んだプログラムを実践的に構築していく研究を行っています。

主な研究業績

1. D. Ishii, N. Yonezaki, A. Goldsztejn. Monitoring Temporal Properties using Interval Analysis. IEICE Trans. Fundamentals, E99-A(2):442–453, 2016.
2. D. Ishii, A. Goldsztejn, C. Jermann. Interval-based projection method for under-constrained numerical systems. Constraints, 17(4):432–460, 2012.
3. D. Ishii, T. Yabu. Computer-assisted Verification of Four Interval Arithmetic Operators. J. of Comp. and Applied Math., 377:1-13, 2020.