社会を支える重要システムの
安全性・信頼性を最先端の科学で実現する

青木研究室　AOKI Laboratory
教授：青木 利晃（AOKI Toshiaki）

E-mail：
［研究分野］
ソフトウェア工学、ソフトウェア科学、形式手法、形式検証、テスト
［キーワード］
モデル検査、定理証明、形式仕様記述、組込みシステム、車載システム、産業応用

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

「ソフトウェア＝プログラム」ではないので注意すること。プログラミング能力よりは、論理的思考能力、抽象化能力が重要です。たとえば、物事を三段論法的に考えたり、複雑な問題をシンプルな枠組みで説明する能力などです。

この研究で身につく能力

現在の社会において使われているシステムや開発されているシステムを対象に、その問題を識別、問題の根本的な原因を明らかにし、理にかなった科学的な解決策を提案できるようになります。日々のニュースや新聞で見聞きするように、現在の産業界では、安全性・信頼性に関する、とても大きな問題を抱えています。この問題を解決するためには、机上だけの科学技術では不十分であり、実際に実践できる科学技術が必要です。企業に入ってしまうと目の前の製品開発で手一杯になりますが、その前に、現実的なシステムの問題を科学的に解決できる上記のような能力を身につけることはとても重要です。そして、これにより、社会において安全、安心を科学技術で支える人材になることが期待されます。

【就職先企業・職種】 製造業、情報通信業、ITコンサルティング会社

研究内容

［正しいソフトウェアの実現へ］

我々が日常生活をしている今日の社会には、様々な所にソフトウェアが使われています。ソフトウェアはパソコンで動作させる物だけでなく、携帯電話、電化製品、自動車、飛行機などにも組込まれており、身の回りの製品、日々の生活に深く関わっています。そのため、ソフトウェアの誤りは日常生活や経済活動を混乱させ、莫大な時間的、金銭的損失を引き起こす可能性があり、実際、そのような事例が報告されてきています。なぜ、誤りを含むソフトウェアが市場に出回っているのか不思議に思う人もいるかもしれません。誤りのない正しいソフトウェアを実現することは現代の科学をもっても達成できておらず、現状では、製品に誤りが含まれてしまうことは不可避なのです。そこで、誤りのない、正しいソフトウェアを開発する方法を確立することは、挑戦的な研究であり、今後の社会の発展、および、安心した生活を送るためにとても重要です。

［形式手法・形式検証］

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

［産業応用への挑戦］

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

主な研究業績

1. Toshiaki Aoki, Daisuke Kawakami, Nobuo Chida, Takashi Tomita: Dataset Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems,25th IEEE Pacific Rim International Symposium on Dependable Computing, pp.100-109, 2020.
2. Toshiaki Aoki, Makoto Satoh, Mitsuhiro Tani, Kenro Yatake, Tomoji Kishi: Combined Model Checking and Testing Create Confidence - A Case on Commercial Automotive Operating System, Chapter 5, pp.109-132, Cyber-Physical System Design from an Architecture Analysis Viewpoint: Springer, 2017.
3. Toshiaki Aoki, Kriangkrai Traichaiyaporn, Yuki Chiba, Masahiro Matsubara, Masataka Nishi and Fumio Narisawa: Modeling Safety Requirements of ISO 26262 using Goal Trees and Patterns, International Workshop on Formal Techniques for Safety-Critical Systems, Springer, pp.206-221, 2015.