本文へジャンプ

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

石井研究室 ISHII Laboratory
准教授:石井 大輔(Ishii Daisuke)

E-mail:
[研究分野]
ソフトウェア工学(形式手法)、制約プログラミング
[キーワード]
サイバーフィジカルシステム、組込みシステム、モデル検査、プログラム検証、区間解析

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

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

この研究で身につく能力

次世代のセーフティクリティカルシステム(例:自動車、ブロックチェーン)を設計・実装・検証するための理論・技術を学修します。研究テーマの本質的な問題点をとらえ、適切に対策を打ち出す能力を身につけます。扱う理論・技術について国際的な研究開発コミュニティ内での位置付けや歴史を知り、広い視野に立ち研究する能力を磨きます。研究テーマに関して何らかのソフトウェアを構築し、現実的な例題に対して実践可能にすることを目指します。また、研究成果の対外発表を通して専門内外の人々に論理的に説明する能力を身につけます。

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

研究内容

 たとえば自動車やロボットといったシステムを、連続変化と離散変化をするハイブリッドシステムと見立て、その高水準・高信頼な設計・実装・検証を可能とする手法について研究しています。また、そのための道具として、数値的な制約(例:連立不等式)を宣言的に記述し、高信頼な求解をおこなうための数値制約プログラミング技術の研究に取り組んでいます。

(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. T. Yabu, D. Ishii. Machine-Aided Verification of Four Interval Arithmetic Operators. Proc. SCAN Conf., pp. 176–177, 2018.

研究室の指導方針

研究者が行う作業(例:サーベイ、問題の定式化、システム開発、実験、対外発表)を各メンバーがひと通り体験し、それら作業のための基本的能力を身につけることを目指します。研究では、対象システム(例:自動車、ロボット、数値計算プログラム)に関して何らかの解析をおこなう方法論やツールを開発します。システムを設計・実装するとともに、メタな仕様記述等を用意し、当該システムの機能・振る舞い・性能・品質等を他人に論理的に説明できることが大事だと考えています。

[研究室HP] URL:http://www.dsksh.com/

ページの先頭へもどる