UPPAALによるAutowareの形式検証

TIER IV 2023 / 03 / 13 UPPAALによる Autowareの形式検証 神戸隆太（TIER IV）

TIER IV 自己紹介 ● ● 神戸 隆太（かんべ りゅうた） 経歴 ○ ○ ○ ○ ● ティアフォーでの仕事 ○ ○ ○ ● 東京大学 工学部（モンテカルロ法に関する研究） 東京大学大学院 コンピュータ科学専攻（型システムに関する研究） ゲーム会社（アルゴリズムの開発・実装） 2022.7~ TIER IV Autowareをひたすら速くする 形式検証やる OS作る その他 ○ ○ ○ 競技プログラミング(AtCoder) ランニング スマブラ強いで

TIER IV 01 / 概要 02 / 形式検証とは UPPAALによる Autowareの形式検証 03 / Autowareでの形式検証実例 04 / 形式検証と開発現場を繋ぐ 05 / まとめ

概要 01

TIER IV Autowareを安全にしたいんじゃ！ ソフトウェアが安全である、とはなにか？ ● ● ● ● ● ● 設計段階で穴がない 実装が設計に忠実 ソースコード由来のバグがない アルゴリズムが正しい リアルタイム制約を満たす etc… 設計段階でバグを引き起こさないことを 理論的（数理的・記号的）に示す 形式手法による安全性向上を目指す！

TIER IV 今回話すこと・話さないこと ◯話す ○ ○ ○ 形式手法とは何か、何ができるのか AutowareにUPPAALを適用した事例 形式手法と開発の架け橋になるには ✕話さない ○ ○ ○ ○ 論理学(時相論理)の解説 形式手法に関する理論研究 UPPAALの使い方 UPPAALによるモデル化の詳細

形式手法とは 02

TIER IV 形式手法とは システムをModel化し、 あるSpecificationを満たすか調べるもの *形式手法は大きくモデル検査と定理証明に別れますが、本発表ではモデル検査のことを指して使います Model： Specification： 状態遷移システム、 オートマトン、 プログラム、etc X Y 〇〇論理(ex 命題, 述語, 様相) で記述される論理式 Z A[]. Y -> Z (Yの後にZに移ることがあるか？ )

TIER IV よくある勘違い Q：ソースコードをツールに投げると正しいか検査してくれるの！？ A：おしい！ ソースコードではなくそれを抽象化したモデルを渡す＋ 「正しい」とはなにかを自分で定義する必要がある 記述！ Specification 形式検証 ツール ソースコード Model 変換！

TIER IV UPPAALとは モデル検査ツールの一種 Model：Timed Automata (時間を表せるオートマトン) Specification：Timed Computational Tree Logic （述語論理 + 時相性を表す[]と<>） 例：2人が2つのドアをランダムに開けるシステム

Autowareでの形式検証実例 03

TIER IV Autowareと形式検証 ● Autowareとは ○ ● 我らが自動運転ソフトウェア！ Autowareを形式検証する...？ ○ 巨大すぎて僕一人では無理です ■ ○ （いずれ全部やりたいが、、） Autowareのようなロボットソフトウェアを UPPAALで検証した先行研究は一応ある(see Appendix) Autowareの中でも特に安全性が求められる 「緊急停止機能(MRM)」をまずは形式検証しよう！

TIER IV 緊急停止機能(MRM)の仕様 MRM：Minumum Risk Maneuver 仕様 ● ● ● ● ● ● ● ● 危険レベルは3種類：0(安全), 1(危険), 2(超超超危険) MRM状態は3種類：Normal, Operating, Succeeded MRM実行状態は3種類：None, Latent(緩停止), Sudden(急停止) 自動のときのみMRMが発動 危険レベル1のときは、すぐにMRMを発動せず、人にTakeover指示を出す x秒間Takeover指示に反応しない場合、MRMが発動 危険レベル2のときは、Takeover中でもMRMが発動 etc… 多すぎる！基本部分から徐々にモデル化していこう！

TIER IV MRMのモデル化 step1 仕様 ● ● 危険レベルは2種類：0(安全), 1(危険) MRM状態は3種類：Normal, Operating, Succeeded E<> MRM_state.SUCCEEDED (いつかはSUCCEEDEDに到達する) OK!

TIER IV MRMのモデル化 step2 追加仕様 ● ● 危険レベルは3種類：0(安全), 1(危険), 2(超超超危険) MRM実行状態は3種類：None, Latent(緩停止), Sudden(急停止) ○ 危険レベル2になったら、緩停止中でも急停止に移行 A[] SINGLE_POINT_FAULT imply SUDDEN_STOP (超危険なら必ず急停止している) E<> LATENT_FAULT imply SUDDEN_STOP (危険レベル1だとしても急停止していることがある) OK!

TIER IV MRMのモデル化 step3 追加仕様 ● ● ● 危険レベル1のときは、すぐにMRMを発動せず、人にTakeover指示 10秒間Takeover指示に反応しない場合、MRMが発動 危険レベル2のときは、Takeover中でもMRMが発動 E<> COMFORTABLE_STOP (緩停止状態に到達することができる) A[] SINGLE_POINT_FAULT imply (not TAKEOVER_REQUESTING) (超危険ならTakeover待ち状態ではない) OK!

TIER IV MRMのモデル化 step4 追加仕様 ● ● システムは、 Timer駆動で状態が遷 移する 一定時間Timerが起動 しなかったら、自動で MRM発動

TIER IV MRMのモデル化 step4 追加仕様 ● ● システムは、Timer駆動で状態が遷移する 一定時間Timerが起動しなかったら、自動でMRM発動 検証が失敗する例 A[] OPERATING imply (COMFORTABLE_STOP or SUDDEN_STOP) (MRMがOperatingなら、緩停止か急停止している) タイムアウト時に状態だけ更新して、操作を更新していないバグ（定義漏れ）

形式検証と開発現場を繋ぐ 04

TIER IV 形式検証と開発現場の乖離 (個人の主観多めです！) 形式検証界隈 開発現場 ● 汎用的なModelで色んな場面 を一括で扱えるよう、オートマト ンの理論を発展させていくぞ〜 ● 新規機能開発、バグ修正、忙し い、、、理論の保証しなくても多 分動くからヨシ！ ● 色んなSpecificationを書けるよ う論理学を発展させていくぞ〜 ● 形式手法...？あ〜オートマトンと か命題論理とか学生の時やっ たなぁ。そんな難しいのわから ないよ

TIER IV 形式検証を含めた開発プロセス 設計 設計 FB Model化 ・・・ 検証 検証 よくある勘違い 設計 実装 検証 実装

TIER IV バグの9割は「Model化」で見つかる（体感） 設計 設計 FB Model化 検証 ・・・ 実装 検証 Model化する時点で、状態遷移が厳密に定まっている必要がある ここが曖昧なことによるバグが多い

まとめ 05

TIER IV まとめ ● 形式検証とは？ ● ● ● ModelとSpecificationを入力とし、正しいか判定する システムをModel化するのも、 それが満たすべきSpecificationを書くのも、人である Autowareに形式検証を適用した ○ ○ Autowareで特に安全性が求められる緊急停止機能(MRM) UPPAALで徐々にMRMをModel化した例を紹介

TIER IV 今後の方針 ● 形式検証とこれからどう付き合っていく？ ● ● ● 自動運転に安全性の理論保証は欠かせないだろ 設計フェーズに形式検証をどんどん取り入れていきたい とはいえ、一気にすべてできるわけではない ● ● ● 検証すべき箇所・検証しやすい箇所はどこか？ 検証ツールはUPPAALが最適？TLA+？SPIN？ 設計だけでなく、アルゴリズムの正しさとかも検証したい ティアフォーでは形式検証に興味のある方も募集しています！ あと、UPPAALでのモデル化初めてだったので、つつけば大量のボロが出てきますｗ

Appendix 06

TIER IV UPPAALによるROS2アプリケーションの形式検証 「Formal Verification of ROS-based Robotic Applications using Timed-Automata」(R. Halder, et al) https://repositorio.inesctec.pt/server/api/core/bitstreams/6c24010f-ef99-4c69-b317-27d5ca42273d/content 要約 「本研究はROSのpub/subの仕組みをtimed-automataでモデル化し， UPPAALというモデル検査器で検証を 行った．単純な pub2-sub1のモデルと，Kobukiロボットという実モデルで検証．例えば， Nodeの構成，subの頻度 ，callbackのlatencyなどが与えられると，そのシステムで特定の性質を満たすか（ ex: pub/subのqueueがoverflow しないか）を検証できる．」

• https://repositorio.inesctec.pt/server/api/core/bitstreams/6c24010f-ef99-4c69-b317-27d5ca42273d/content