研究背景・目的

　今日、製造業においては高度な情報処理技術を用いた自動化とソフトウェア支援により、設計から生産までの製造工程のあり方を根本的に変える取り組みが進んでいます。この背景を踏まえ、従来、ソフトウェア開発に用いられてきた「形式手法」と呼ばれる数学的手法を工業製品の開発に適用し、製品の信頼性や開発効率を画期的に向上させることは、それらが計算機制御され、その機能・複雑さ・社会的責任を増している今日、学術的・産業的に非常に重要なトレンドとなっています。本研究では、JST ERATO「蓮尾メタ数理システムデザインプロジェクト」を通して先進的形式手法の研究、さらに産業界の実問題に対する応用・実装を進め、形式手法の効果実証、実用化をめざすことを目的としています。

研究内容

　形式手法を自動車制御などの物理情報システムに適用するためには、従来、コンピュータでの計算を前提として扱ってきた「離散的要素」と物理系の連続ダイナミクスや確率・時間などの「連続的要素」の両方を包含するような理論拡張が必要となります（図1）。私たちは独自のアプローチとして、形式手法の拡張過程そのものを「論理学」「圏論」といった抽象数学を駆使して解析、高次（メタレベル）の理論を構築し形式手法の諸技法を一挙に拡張します（図2）。一方、応用面では、これらの理論研究の成果を制御理論、最適化理論を用いて具体化、また機械学習などの実践的ソフトウェア工学手法を活用して実用化をめざします。

産業応用の可能性

　この研究では産業応用志向が一つの特徴です。具体的な方向性として二つのアプローチで進めています。一つ目のアプローチでは国内外の企業と協働し、実際の製品設計プロセスに対し形式手法の支援を行います。ここでは現状の開発プロセスに適用することで、具体的・実践的な形式手法の適用実現とその効果を実証します。二つ目のアプローチは、将来の製品設計プロセスにおける形式手法の果たす役割を追求します。ここでは、ソフトウェアを中心とした先駆的な製品設計プロセスを実践するカナダのウォータールー大学の自動運転車プロジェクトをテストベッドとして形式手法の産業応用について先駆的研究を行います。