2024-04-10 国立情報学研究所
大学共同利用機関法人 情報・システム研究機構 国立情報学研究所（NIIエヌアイアイ、所長：黒橋くろはし 禎夫さだお、東京都千代田区）のアーキテクチャ科学研究系教授 蓮尾はすお 一郎いちろうと、京都大学（総長：湊みなと 長博ながひろ、京都府京都市）大学院情報学研究科助教 和賀わが 正樹まさきらの研究グループは、科学技術振興機構（JSTジェイスティー、理事長：橋本はしもと 和仁かずひと、東京都千代田区）の戦略的創造研究推進事業 ERATOエラトー蓮尾メタ数理システムデザインプロジェクト（*1）（ERATO MMSD、研究総括：NIIアーキテクチャ科学研究系教授 蓮尾 一郎）などのもと、自動運転車の安全性保証の枠組みである国際標準ISO 34502（*2）で示された危険シナリオ群について、その意味内容の数学的定式化を行いました。
本研究では、従来英語などの自然言語で記述された危険シナリオを「STL（シグナル時相論理、Signal Temporal Logic）（*3）」という形式言語で記述することで、解釈の違いが生じる可能性がある危険シナリオの意味内容を確定させ、また危険シナリオを用いた安全性評価タスクの自動化・効率化を可能にしました。本成果は自動運転車の安全性保証に貢献する成果であり、また同時に、情報システムと人間社会との間の「契約」たる要求仕様の活用において、数学が果たしうる重要な役割を指し示すものでもあります。
本研究成果を、情報学応用に関する主要国際会議The 39th ACM/SIGAPP Symposium On Applied Computing（SAC）2024で、2024年4月9日（中央ヨーロッパ時間）発表しました。
【ポイント】
- 自動運転車の本格普及に向けて、広範・詳細な安全性保証による社会的信頼の樹立が急務である。
- この目的に向けて、ISO 34502は自動運転車の危険シナリオ群を網羅的に定めている。しかし自然言語で記述されているため、意味内容に解釈の違いが生じる可能性があり、ソフトウェアツールによる機械的処理が容易ではなかった。
- 本研究では、「STL」という形式言語を用いて、ISO 34502の危険シナリオ群を数学的に定式化した。これにより危険シナリオ群の意味内容を確定させ、モニタリングなどの安全性評価タスクの自動化・効率化が可能になった。
- 自動運転車の安全性保証に貢献する成果であり、また一般に、自動運転をはじめとする新技術の社会受容に向けて数学が果たすべき重要な役割を指し示す成果でもある。
【背景】
今後の社会に期待されている自動車の自動運転技術の普及のためには、自動運転車の安全性を高めるだけでは十分ではありません。高い安全性を社会に対して保証しそれを説明して、自動運転車を公道に受け入れてもらう必要があります。国内外でさまざまな安全性保証の枠組みが提案されていますが、その中でもISO 34502は、一般財団法人日本自動車工業会（以下、日本自動車工業会）の取り組みを起源とする日本発の安全性保証の枠組みです。
ISO 34502では、自動運転車の動作を「認知」「判断」「動作」の3段階に分けたのち、各段階における危険要素を同定してそれらの組み合わせを考えることにより、自動運転車の危険シナリオを網羅的に列挙しています。これらの危険シナリオにおいて適切な安全行動をとれるかどうかを評価することにより、自動運転車の安全性を保証しようというのが同規格の考え方です。
しかしISO 34502では、これらの危険シナリオが自然言語（英語）で記述されており、その大規模応用の妨げになっていました。その１つ目の問題は自然言語の曖昧さであり、たとえば「強引な割り込み」が正確には何を指すのかについて、解釈の違いが生じてしまっていました。
２つ目の問題はソフトウェア処理の困難さです。危険シナリオ群を用いた安全性評価においては、モニタリング（走行データにおける危険シナリオの発生を検知する）や、テストデータ生成（危険シナリオが生じるような走行状況をシミュレーション用に生成する）などの安全性評価タスクを大量に実行する必要があり、ソフトウェアによる自動化が必須です。しかし自然言語で記述された危険シナリオに対しては、これらタスクを実行するソフトウェアをシナリオごとに改めて一から作成しなければならず、多大な労力がかかってしまいます。
【研究手法・成果】
本研究では上記の問題を解決するため、ISO 34502の危険シナリオ群のうち、特に「判断」段階の危険要素に起因するシナリオ群（図１）に対して、これらの数学的定式化を行いました。この定式化により危険シナリオそれぞれに「数学的定義」を与え、その意味内容を確定させました。
（図1） ISO 34502の危険シナリオ群のうち、特に「判断」段階の危険要素に起因するものの一覧。
表はISO 34502:2022からの引用。
この数学的定式化（図２）のためにSTLを用いました。プログラムを書く際にプログラミング言語という形式言語を用いるのと同じように、STLという形式言語を用いて危険シナリオを記述していくことになります。そうすると、STLの語彙それぞれの意味がすでに数学的に定義されているため、危険シナリオの意味が数学的に定義できます。さらにこの定式化においては、本研究グループが開発中の対話型ツール「STLデバッガ」を用いて、記述した数学的内容がISO 34502のもともとの意図に合致しているかを確認しながら、定式化を進めていきました（図３）。
（図２） 本研究の成果たるISO 34502危険シナリオ群のSTLによる数学的定式化の例。各危険シナリオscenarioi（i=1,2,…,24）のテンプレートとその構成要素を表で示している。
（図３） 「STLデバッガ」のスクリーンショット。左上のテキスト部で入力したSTL論理式の意味内容を、右側のGUI部で対話的に確認することができる。
STLを用いた数学的定式化は、上記の２つ目の問題も解決します。STLを入力フォーマットとしてモニタリングやテストデータを生成するアルゴリズムは（本研究グループのこれまでの研究成果も含め）多数存在しますが、今回の研究成果により、これらのアルゴリズムがISO 34502の安全性評価に適用できるようになります。
【今後の展望】
STLは製造業における広い応用が期待されている形式言語であり、STLに基づく品質保証ソフトウェアツールのエコシステムが形成されつつあります。今回の研究成果は、このソフトウェア・エコシステムと自動運転車の安全性保証のための枠組み（ISO 34502）の２つをつなぐものであり、両者の発展をさらに促進して、自動運転の社会受容のみならず、製造業の設計過程の自動化・効率化をも推し進めるものです。
一方、STLの産業界活用の1つの障壁として、STLに習熟した技術者でないと意図した内容を容易に記述できないという問題がありました。STLは決して難しい形式言語ではありませんが、それを学ぶためには新しいプログラミング言語を学ぶのと同様の学習過程が必要になります。今回用いた「STLデバッガ」は、一般的なプログラミング言語のデバッガと同様の役割を果たすものであり、STLの学習過程を助け、その産業界での活用を推し進めるものです。
本研究の定式化では、危険性を定義するために、RSS（責任感知型安全論、Responsibility-Sensitive Safety）（*4）安全距離の概念を用いています。RSSは自動運転車の安全性を数学的に証明する方法論として注目を集めており、本成果を通じてRSSの活用の場面がさらに広がっていくことが期待されます。
より一般には、さまざまな情報システムの性質・要求仕様・動作シナリオなどを数学的に定式化することは、意味内容の明示化やデータ処理の自動化を可能とさせ、信頼性が高く、効率的な製品開発に貢献できるため、大きな産業的・社会的意義を持ちます。このような数学の社会応用の一つのあり方を広く発信し、またこれを支える技術とソフトウェアツールをさらに発展させることで、情報システムの信頼性樹立と社会受容を実現すべく、研究を続けていきます。
蓮尾 一郎 教授からのコメント：
「本研究の契機は三菱電機株式会社様との協働であり、STLによる要求仕様の数学的定式化のケーススタディとしてISO 34502を提案いただいたことにより、本成果が可能になりました。 自動運転システムや生成AIなど、新しい情報技術には『十分に安全か、社会に受け入れてよいほど安全か』という社会的信頼の問題が常につきまといます。その際、情報システムが満たすべき要求仕様は『社会との契約』であり、社会的信頼の基盤になるものですから、本研究のような数学的定式化は非常に重要です。今後、情報技術と社会との関わりを整理し情報技術を安全に使役する人間中心の社会を実現するために、数学的技術の研究開発をさらに進めていきます。」
【研究プロジェクトについて】
本研究は、科学技術振興機構（JST） 戦略的創造研究推進事業 ERATO「蓮尾メタ数理システムデザインプロジェクト」（JPMJER1603）、JST 研究成果展開事業 大学発新産業創出プログラム START プロジェクト推進型 起業実証支援「ソフトウェア品質の論理的説明技術による、自動運転の本格普及の実現」（JPMJST2213）、JST 戦略的創造研究推進事業 CREST「AI集約的サイバーフィジカルシステムの形式的解析設計手法」（JPMJCR2012）の一環で行われました。また本研究では、三菱電機株式会社情報技術総合研究所との協働も行いました。
【論文タイトルと著者】
タイトル：Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance
著者：Jesse Reimann, Nico Mansion, James Haydon, Benjamin Bray, Agnishom Chattopadhyay, Sota Sato, Masaki Waga, Étienne André, Ichiro Hasuo, Naoki Ueda, Yosuke Yokoyama
発表会議：The 39th ACM/SIGAPP Symposium On Applied Computing (SAC) 2024
発表日：2024年4月9日（中央ヨーロッパ時間）
News Release: PDF
ISO 34502の自動運転車危険シナリオを数学的に定式化
～安全性保証タスクの自動化・効率化により自動運転の社会受容を促進～
【用語解説】
*1 ERATO蓮尾メタ数理システムデザインプロジェクト：国立研究開発法人 科学技術振興機構（JST）の「戦略的創造研究推進事業ERATO」に採択されている研究プロジェクトで、Society 5.0の大きな柱となる物理情報システム（CPS）の品質保証手法の学術的研究を推進している。特に、CPSの典型例の一つとして注目される自動運転システムを重点応用対象として、その信頼性保証を支えるモデリング手法・形式検証手法・テスト手法、さらにこれらを包括する実用的な 検証と妥当性確認（V&V）技術の研究開発に取り組んでいる。このような大きなチャレンジでは、ソフトウェア・制御・AI といった多様な学術分野の協働が必要となるため、学術分野融合の基礎となる数理的（メタ）理論も重視して研究を推進する。略称はERATO MMSD。プロジェクト詳細はhttps://www.jst.go.jp/erato/hasuo/ja/参照。2022年3月に本研究期間を終了し、現在は追加支援期間として研究を推進中（2025年3月まで）
*2 国際標準ISO 34502：日本自動車工業会の「自動運転の安全性評価フレームワーク」を起源とする日本発の自動運転車の安全性保証の枠組みの提案。詳細は経済産業省のニュースリリースを参照 https://www.meti.go.jp/press/2022/11/20221116006/20221111005.html
*3 STL（シグナル時相論理、Signal Temporal Logic）：∧（かつ）、∨（または）などの演算子を持つ基本的な論理体系である命題論理に対し、F[0,T]（これからT秒以内に）、G[0,T]（これからT秒間ずっと）などの時相演算子を加えて拡張して得られた時変シグナルの性質を記述するために適した論理体系。O.MalerとD.Nickovicにより2004年に導入された。
*4 RSS（責任感知型安全論、Responsibility-Sensitive Safety）：Mobileye社の研究者が最初に提唱した自動運転車の安全性に数学的証明を与えるための方法論。追突回避という特定の運転シナリオに適用すると、適切にブレーキをかけることで必ず追突を回避できるような車間距離（RSS安全距離）の公式が得られる。2022年のERATO MMSDの研究の成果により、レーン変更や非常停止といった複雑な運転シナリオへも適用が可能となった。詳細は以下のニュースリリースを参照。 https://www.nii.ac.jp/news/release/2022/0707.html
