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

サイバーフィジカル制約プログラミング研究室　
Laboratory on Cyber-Physical Constraint Programming
准教授：石井 大輔（ISHII Daisuke）

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

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

数学の基礎知識、プログラミング能力、英語力を有しているのが望ましいですが、専門的な知識・能力は配属後に学び始めても問題ありません。目標達成に向けて努力を惜しまない学生を歓迎します。

この研究で身につく能力

安全性が求められるサイバーフィジカルシステム（以下「CPS」）について、モデル化・設計・実装・検証を行うための理論と技術を学修します。CPS中のソフトウェア品質保証を目的に、独自手法の提案、ツールの実装、実験に取り組みます。これにより、CPSとソフトウェア関連の幅広い職業で役立つ基礎的な能力を習得することができます。また、サーベイ、問題の定式化、実験、対外発表など、研究者が行う主要な作業をひと通り体験し、それらに必要な基本能力の習得を目指します。

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

研究内容

　自律走行する車、発電所、医療機器など、実世界の多くのシステムは、サイバー（情報）部品とフィジカル（物理）部品がセンサーとアクチュエーターを介して相互作用するCPSとみなせます。本研究室では、安全で高信頼なCPSの構築を目指し、「制約」の概念を用いた方法論や技術の研究に取り組んでいます。制約とは、特定の領域における関係を記述するもので、たとえば、命題変数をもつ論理式、実数変数をもつ連立方程式、車の状態変数をもつ交通ルールなどが挙げられます。これらの問題を宣言的かつ論理的に記述したり、効率的に解いたり、わかりやすく説明したりすることを目指しています。

[研究事例1] CPSのモデリング・シミュレーション・検証

【モデリング】CPSを簡潔・直感的に記述するための言語 (例：ハイブリッドオートマトン、時相論理式、Simulink図) について、記述実験をしたり、意味論や相互の関係を調べたりしてきました。
【シミュレーション】CPS開発では、モデルの振る舞いの数値シミュレーションが有用ですが、数値誤差やその他の原因による不具合が問題となります。精度保証計算や記号計算による高信頼化に取り組んでいます。
【検証】CPSモデルや実装の網羅的なテスト・検証手法について研究しています。制約ソルバーによる安全性の検証 (業績1)、モデル分割による検証の効率化 (業績2)、テストケース自動生成などに取り組んでいます。
【応用】上記技術を自動運転プラットフォームAutowareに応用するプロジェクトに参画しています。

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

　実数領域の制約について、充足解や最適解を求める制約ソルバーの開発に取り組んできました。提案ソルバーは区間解析に基づくのが特徴で、結果について数値的な精度保証をしたり、不確実値を含んだまま求解したりすることが可能です。また、CPSモデル検査のために、数値変数をもつ述語論理式を精密に扱うSMTソルバーを開発しています (業績3)。

主な研究業績

1. D. Ishii, 他. SMT-Based Model Checking of Industrial Simulink, International Conference on Formal Engineering Methods (ICFEM), LNCS 13478, pp. 156-172, 2022.
2. D. Ishii. A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method, International Symposium on Model Checking Software (SPIN), LNCS 14624, pp. 67–84, 2024.
3. D. Ishii, T. Tomita, T. Aoki. Approximate Translation from Floating-Point to Real-Interval Arithmetic, NASA Formal Methods, LNCS 13260, pp. 733-751, 2022.