正しいソフトウェアを実現する研究は計算機科学の歴史において、比較的長く行われています。代表的なものとして形式手法（Formal Methods）、形式検証（Formal Verification）があります。形式手法・形式検証では、数学を基礎とした言語やツールを用いて、対象となるソフトウェアを記述し、検証を行います。これにより、なんとなくソフトウェアを開発するのではなく、数学に基づいた解析や正しさの保証を行うことができます。ここでの正しさは理論的な観点のものであり、実製品での正しさ、安全性、信頼性とはギャップが大きいです。それでも、現在のところ、実製品としての正しいソフトウェアを実現するための有望なアプローチであると言えます。また、このような手法を用いて、ソフトウェア自身を科学することも重要です。ソフトウェアがこれからの社会や世界の構成要素であり続けるのであれば、他の自然科学の学問分野と同様、その本質や原理を明らかにして、事実を積み上げ、共有し、発展させる必要があります。そこで、本研究室では、形式手法・形式検証を用いて正しいソフトウェアを開発する手法、および、ソフトウェア開発の原理に関する研究を行っています。

現在の社会においてソフトウェアは重要な構成要素です。本研究室の研究対象は、「社会におけるソフトウェア」です。そのため、企業との共同研究を積極的に行っています。これまでに、主に、自動車（車載システム）を対象として、共同研究を行ってきました。現代の自動車は、多くの部分が電子制御されており、ECU（Electronic Control Unit）と呼ばれるコンピュータが多く使用され、ネットワークで接続されて協調動作しています。ハイエンドの自動車では、100個を超えるECUが使われており、非常に複雑なシステムになっています。一方で、自動車は我々の身近にある危険な乗り物であり、毎年、多くの人命が交通事故などで失われています。そこで、ソフトウェアを用いて正しく制御することはもちろん、高度な安全性の実現への挑戦がなされています。自動車において、ソフトウェアの役割は、非常に重要なものとなっているのです。我々は、車載システムメーカや研究所と共同研究を行い、実製品の検証に成功している世界的にも数少ない研究室の1つです。さらに、近年、自動運転の実現にAIが使用され、画像、動画などの情報を入力として、認知、判断、操作を行うようになりました。このような複雑な入力、および、AIによる不確実性を伴う判断結果をどのように取り扱うかが大きな課題になっています。車載システムに限らず、ソフトウェアの応用先は多様化しています。DX、ブロックチェーン、スマートシティといったキーワードが注目されていますが、ソフトウェアは、それらを実現する重要な基盤となります。我々は、今後も、様々な分野で、社会を支える重要システムの安全性・信頼性を最先端の科学で実現し、安全・安心な社会を目指して研究を行っていきます。

ソフトウェアは益々多様化してきています。現在流行っているAIと呼ばれるものも、ソフトウェアとして実現されています。自動車の自動運転においても、ソフトウェアが果たす役割は大きいです。また、社会的にDX、デジタル化が、叫ばれていて、ソフトウェアは、それらを実現する重要な基盤です。我々は、このような近代的システムを対象として、研究を行っています。以下に研究テーマの例を示しておきます。

• AI搭載システムの信頼性・安全性の検証手法に関する研究


• 画像や動画など複雑なデータに関する仕様作成手法、および、検証手法に関する研究


• 近代的オペレーティングシステムの検証手法に関する研究


• MATLAB/Simulinkを用いたモデルベース開発における検証手法に関する研究


• 車載システム向けプログラムの実践的検証手法に関する研究


• オープンソースの品質保証に関する研究


• ブロックチェーン技術に基づいたシステムのリスク評価手法に関する研究


• 宇宙機を対象としたモデルベース開発に関する研究


• モバイルファイルシステムの信頼性・安全性検証手法に関する研究


• 量子計算の古典プログラム検証への応用に関する研究