第１回 FMAPセミナーのご案内．

以下のように第１回 FMAPセミナーを開催いたします．学生の皆様，教職員の皆様，どなたでも参加可能です．事前登録は必要無いですが，人数が多くなった場合，感染予防の観点から，参加を制限させていただくことがあるかもしれません．

皆さん，今年の３月に小松駅と小松空港の間に自動運転バスが運行開始したのをご存知でしょうか？そのシステムにはAutowareと呼ばれるオープンソースソフトウェアが使われています．この度，Autowareを主導している株式会社ティアフォーから高野様と神戸様にお越しいただき，ご講演いただくことになりました．生成AIなどのAI技術が注目を浴びていますが，AIだけではシステムは動作しません．AIを用いた自動運転を支えるシステムソフトウェアに関する興味深いご講演です．
青木利晃(FMAP Project PI)

第１回 FMAPセミナー
タイトル：自動運転システムと形式検証
講演者：高野祐輝，神戸隆太 （株式会社ティアフォー）

日時：2024年5月29日(水)
時間：15:30 – 17:00
場所：大講義室

概要：
・冗長化システムにおけるリーダー選出アルゴリズムの形式検証．
自動運転システムでは、ハードウェアを冗長化することによって、システムの一部が故障した際にも安全を確保する必要がある。ここでは、リーダー選出アルゴリズムを用いて、冗長化によって発生する問題を解決する方法を示す。また、リーダー選出のようなテストのしにくい分散アルゴリズムを、SPINモデル検査器を用いて形式検証した手法を示す。
・Rustによる ROS 2 エグゼキュータの形式検証．
自動運転ソフトウェア「Autoware」は、ROS2というミドルウェアの上で実装されている。ここでは、既存の ROS 2のエグゼキュータを Rustに書き換えることで既存の ROS 2 のエグゼキュータの問題点を解決しつつ、そのプログラムの一部をTLA+ というモデル検査器で形式検証を行なった事例を示す。
・自動運転向け Kernelの設計と形式検証．
ティアフォーでは、自動運転に求められるリアルタイム性とパフォーマンスの追求のため、独自にKernel (OS)を開発している。ここでは、その設計思想を示すとともに、様々な形式検証ツールを使って Kernel の機能を形式検証している事例を示す。

講演者紹介：
高野祐輝 博士（情報科学）
株式会社ティアフォー
アーキテクト/System Software Teamチームリーダー
2001年に石川工業高等専門学校電気工学科を卒業。2003年に石川工業高等専門学校専攻科電子機械工学専攻を修了。2005年に北陸先端科学技術大学院大学情報科学研究科博士前期課程を修了。2011年に北陸先端科学技術大学院大学情報科学研究科博士後期課程を修了。その後、北陸先端科学技術大学院大学高信頼ネットワークイノベーションセンター研究員や、情報通信研究機構サイバーセキュリティ研究所サイバーセキュリティ研究室研究員、大阪大学大学院工学研究科特任准教授などを経て、2022年より現職。著書に『並行プログラミング入門 Rust、C、アセンブリによる実装からのアプローチ』(オライリー・ジャパン)、『ゼロから学ぶRust』(講談社)がある。

神戸隆太
株式会社ティアフォー
System Software Team所属
2022年に東京大学大学院コンピュータ科学専攻を卒業。専門は形式検証。競技プログラミングが好き。