青木利晃 教授
1994年東京理科大学学士（理学）、1996年北陸先端科学技術大学院大学修士（情報科学）、1999年同大学博士（情報科学）。
情報科学研究科助手、安心電子社会研究センター 特任助教授、情報科学研究科助教授等を経て2016年より現職。専門分野はソフトウェア工学、ソフトウェア科学、形式手法、形式検証、テスト。
実用化が加速する自動車の自動運転システム。AI技術を用いた製品やサービス。金融業界で注目を集めているブロックチェーン。社会のあり方を根本から変えるスマートシティー。
ソフトウェアが組み込まれた製品や、ソフトウェアで実現されたシステムによるサービスは、今日の社会になくてはならないものになっています。では、その安全性と信頼性はどのように考えられ、どのように保証されるのでしょうか。本学セキュリティ・ネットワーク領域の青木利晃教授にお話をうかがいました。
形式手法・形式検証を適用し、安全で快適な現代社会の「当たり前」を支える
部屋の中を見回してみると、パソコン、スマホ、カメラ、家電製品など、「動くもの」にはほぼすべて組込みソフトウェアが入っています。さらに自動運転システムやAIシステム、宇宙システムなど、一昔前はなかった大規模で複雑なシステムも登場しており、現在は近代的なソフトウェアへの変遷期にあると言えます。こうした中で半導体需要は伸び続け、世界的に半導体不足が多くの業界の頭痛の種になっているのはご存じのとおりです。
私たちはふだんソフトウェアの存在を意識せずに製品やサービスを利用していますが、実は誤りを含むソフトウェアも少なからず市場に出回っています。実際、ソフトウェアの不具合が製品の故障やサービスの停止を引き起こし、社会の混乱や経済的損失、人的損失につながる事例も起きています。ソフトウェア技術が日常生活を支える社会基盤となっている今、その品質、安全性、信頼性にをいかに保証するかということは重要な課題となっています。
安全で快適な現代社会の「当たり前」を支えるため、当研究室では、形式手法（Formal Method）・形式検証（Formal Verification）を適用して誤りのないソフトウェア、高い安全性、信頼性を持つソフトウェアの実現を目指しています。
形式手法・形式検証は1960年代からヨーロッパを中心に研究や実践が進められてきた分野で、数学を基礎とした言語やツールを用いて対象となるソフトウェアを記述し、検証を行います。企業の開発現場でもレビューやテストを重ねて安全性を検証していますが、こうしたやり方では人手も時間もかかる上、高い品質を達成するのが難しい場合があります。私たちは大学の研究者として、企業とは異なるアプローチ、すなわち科学的な根拠に基づいて安全性、信頼性を保証する、という姿勢を重視しています。
またエンジニアがこのソフトウェアは安全で信頼できると思っていても、ユーザーがそう思っていなければ安心して利用することはできません。そのためソフトウェアの品質をどう科学的に保証するか、安全であることをどう説明するのかという点にも着目しています。数学に基づく形式手法・形式検証は、そういった面でも有利だと考えています。
企業との共同研究を通じ、理論と実践のギャップを埋める
一般的に、形式手法・形式検証は理論面が強く、現場とのギャップが大きいと言われています。対象となるソフトウェアが大規模化・複雑化すればするほど証明は難しくなりますし、問題を解くアルゴリズムが存在しない、いわゆる決定不能問題も相手にしなければいけません。またAIを用いた近代的なソフトウェアは不確実性を含む推論を取り扱うため、不確実性を踏まえた上でどう安全性を担保するかはチャレンジングな課題です。当研究室では企業との共同研究を通じ、こうした理論と実践のギャップから生じるさまざまな問題をクリアすることに取り組んでいます。特に自動車に関しては多くの研究実績があります。
一例を挙げると、日立製作所との共同研究において、形式手法・形式検証に基づいて車載システムの安全要件を曖昧さなく表現し、漏れが無いことを自動検証する手法を構築しました。この成果に基づいて企業側が技術開発を行ったところ、提案手法が実践可能でかつ高い効果があることが確認されました。
車載システム検証（OSEK/AUTOSAR OS/CAN/FlexRay)
また私と、同じく本学セキュリティ・ネットワーク領域の石井大輔准教授、冨田尭講師の３名と、ツールベンダーであるガイオ・テクノロジー社との共同研究で、組込みソフトウェアの検証・開発ツールを開発しました。主に車載ECU（Electric Control Unit）のソフトウェア開発をサポートするパッケージ製品です。
制御システム検証ツール(PROMPT)
ソフトウェアは実社会で広く使われているものですが、形式手法を実際の製品に応用する研究事例はそれほど多くありません。研究活動を実際の製品やサービスに結び付けることは、私の研究ポリシーでもあり、研究のモチベーションともなっています。
ただし実際の製品を相手にするときに、企業の開発現場と同じ方法をとっていては大学の意味がありません。これは学生にも言っていることですが、理論と実践をいかに両立させるか、ということを重視しています。
AI応用システムの安全性、信頼性を保証する技術を確立
これから力を入れていきたいのはAIが絡んだシステムの検証です。AIが暴走して人類が危機にさらされる…というのは古くからある映画やSF小説のテーマですが、それほど派手なものでなくても、機械学習をはじめとするAI技術は、私たちの生活や経済に大きな影響を及ぼすようになっています。今後さらに社会を支える重要システムにAIが組み込まれていく中で、その安全性を保証する技術を確立することは避けて通れない課題です。
情報セキュリティであれば、データの破損や情報漏洩を防ぐというイメージがわきますが、ソフトウェアの安全性、信頼性というと、その成果が社会にどう役立っているかは想像がつきにくいかもしれません。それはソフトウェアは動いて当たり前、安全に使えて当たり前、という認識があるからです。しかし当たり前は当たり前ではなく、企業の存続や人の命を危うくする問題は「ことが生じてから対応する」のでは遅いのです。ソフトウェアの安全性を最先端の科学で保証し、トラブルや事故を未然に防ぐという私たちの研究の意義を、強く広く発信していきたいとも思っています。
令和3年11月掲載
