研究 / Research

物理情報システムの高品質化を支援する「メタ数理システムデザイン」

　科学技術イノベーションの多くは物事の本質を抽象化して理解し、一般的に適用可能な理論を構築することから生まれてきました。機械やソフトウェアの生産現場では、さまざまな数学理論や手法が利用されていますが、その現場の視点からいったん離れ、各種理論や手法を俯瞰して数学的に研究することで、より多くの問題が一度に解決可能な解答が得られることがあります。このような抽象的な数学理論を用いた情報学研究に、私は取り組んでいます。
　その研究の中で近年注力しているのが、国立研究開発法人科学技術振興機構の「Exploratory Research for Advanced Technology：ERATO」プログラムの一つである「メタ数理システムデザインプロジェクト」です。これは自動車をはじめとするコンピュータを搭載した機械（物理情報システム）の仕様策定・設計・実装・保守の各工程の効率化と品質向上の支援を目的とした研究プロジェクトです。

各種の理論の拡張過程を、より高次の理論で一般化

　このプロジェクトは、「形式手法」と呼ばれるソフトウェア科学の数学的な設計技法を、物理情報システムの生産に適するように拡張して応用することを目指しています。形式手法とは、ソフトウェアが目的に沿って機能するか否かを数学的に検証する手法のことです。例えば可達性解析というトピックに注目すると、そこではオートマトンによる解析、抽象解釈、不変量解析など各種の形式手法が利用されており、各手法はそれぞれ自動車の衝突防止システムへの応用が期待できます。しかし、それを実際の自動車に応用するときには、各手法に自動車ならではの連続ダイナミクスや時間、さらに確率の概念を加えた拡張が必要になります。形式手法個々に拡張を図るのは大変ですが、拡張の過程を数学的に解析して、より高次（メタレベル）の一般化された理論が構築できれば、すべての手法にそれを適用して、拡張に要する労力を大きく軽減させることができます。

　このように、製品設計の背景をなす各種の理論を、抽象化された一般的な方法で拡張可能にするのが同プロジェクト内で私が担当している理論グループの役割です。プロジェクト内には他に、理論をもとに具体的な生産に適するよう形式手法を拡張する実務グループと、その結果の拡張された形式手法を生産現場に適用する応用グループがあります。
　私の研究は、いわば既存理論を拡張するための「レシピ」を作る取り組みです。このようなレシピを元にさまざまな形式手法を拡張・改良すれば、それらを適用して生産工程における無駄なプロセスを省くことができます。例えば自動車のテスト工程のパラメータ最適化が可能になり、無駄な入力をせずに済みます。それでたとえ1〜2％でもコスト削減できれば、大量生産製品なら巨額の節約ができるわけです。このようなレシピ作りを丹念に行っていくことで、自動運転の実現をはじめ、各種の物理情報システムのイノベーションに重要な貢献ができるものと思っています。

賢くソフトウェアをつつく・直す－探索・学習によるソフトウェア工学：ERATO-MMSDプロジェクト インテリジェンス協働形式手法グループ

リンク

• [NII SEEDS] 「形式手法」をものづくりへ 高品質・高効率な製品開発に向けて
• [NII Today] 抽象数学で 工業製品の設計支援 - NII Interview (77-1)