第7回 オートモーティブ・ソフトウェア・フロンティア 2022

⾃律⾛⾏⾞と開発プロセス- AI 組込の観点から 伊藤昌夫 (nil@nil.co.jp)
株式会社ニルソフトウェア

⽬次• ソフトウェアにおける形式検証• 仕様の⼀部としてのODD• AI利⽤時のプロセスへの影響• AIの利⽤• プロセス設計• TMカード• まとめ

2022/2/25

NIL2

ソフトウェアにおける形式検証
T ru st w o rt h i n ess

総合的信頼性（特に安全性）のために

2022/2/25

NIL

3

最弱事前条件• プログラム

𝐶 𝑃{𝑆}(1)

Cの状態からPを実⾏するとSの状態になる• 最弱事前条件（weakest precondition）

𝐶 ⇒ 𝑤𝑝(𝑃, 𝑆)(2)

最弱事前条件とは，PによってSが成⽴する上で，最も制約の弱い（少ない）条件

2022/2/25

NIL4

これまでの取り組み︓形式検証
形式検証とは，「数学的なモデルを⽤いて，作られたプログラム（実装）が仕様と合致していることを確認する」こと【補⾜】
多くの安全系の規格は，形式⼿法を使⽤することを推奨しています．
ISO 26262（⾃動⾞），EN 50128（鉄道），DO-178C（航空機）

形式検証の主たるアプローチ︓

LTL︓線形時間論理- モデル検査

取り得る状態の網羅．望まない状態にならないこと（Safety），望む状態にいつかなること（Liveness) を検出．規模の問題がある．プロパティはLTL式(*)で記述．

- 演繹的アプローチ

プログラムの正しさを証明できる．但し，証明可能な範囲には制限がある（証明器の発展により制限は緩和される）．

- 抽象解釈静的コード解析．検証プロパティの指定は基本的に不要．偽陽性を検出する場合がある．

2022/2/25

NIL5

Ada ... SPARK• Ada• 強い型付けを特徴とする静的なプログラム⾔語（最初の規格化は1983年）• 仕様と実装を分離• ⾔語設計時点で，開発環境も考慮（e.g. APSE）• 適⽤例︓Boeing 777• SPARK• Adaの部分的な拡張︓「契約」的設計（AdaのAspects利⽤）• フロー分析／実⾏時検査／正しさの証明（⼀階の述語論理記述による）• 補助⼿段として，他に契約ケース・ゴーストコード等がある• 適⽤例︓Euro Fighter，C130J

2022/2/25

NIL

6SPARK形式検証例︓仕様部
パッケージが基本単位

SPARKコードであることを明⽰

証明したいこと（表明）

仕様部︓⼿続き Increase と事後条件

2022/2/25

事後条件では，⼿続きが終了したときに成⽴しているべき条件を⽰す．ここでは，⼊⼒Xの値が変数Cより⼩さいならば，出⼒Xは，⼊⼒Xより必ず⼤きくなり，それ以外の条件では変数Cの値に等しいことを仕様として⽰している．これが，⼿続き利⽤者との「契約」となる．
なお，XʼOld は，この⼿続きを実⾏する前の⾃然数Xの値のこと．X は in out パラメータであり，値が変化する
NIL7

違いは何か︖• そもそもが前提条件が難しい• ⾃律⾛⾏⾞においては，ODDの設定は典型的な例である

𝐶 ⇒ 𝑤𝑝(𝑃, 𝑆)

2022/2/25

(2)

NIL

8

仕様の⼀部としてのODD

2022/2/25

NIL

9

Definition of ODD in J3016:2021 and SHs
Definition

3.21 Operating conditions under which a given driving
automation system or feature thereof is specificallydesigned to function, including, but not limited to,environmental,geographical,
andtime-of-day
restrictions, and/or the requisite presence or absenceof certain traffic or roadway characteristics.

Geography
2022/2/25

Environment
NIL

Time-of-day

Car, Pedestrian ..
10

ODDのさまざまな利⽤者
開発側に関わらず，利⽤者や法的執⾏機関もまた理解する必要がある
Public (User)
Availability, Usability

Manufacture(Developers)

OEM2022/2/25

Supplier

Business request
Technical reasons
Design/Test

Owner

ODD

Passenger
NIL

Legal request

Lawmaker

Regulators

Government

Jurisdiction
11ODD記述法に関する幾つかの規格・⽂書
#ID

Title

Issued byDate

BSI PAS 1883

Operational Design Domain (ODD) taxonomy
for an automated driving system (ADS) –Specification

BSI

31.Aug.
2020

WISE

Operational Design Domain for AutomatedDriving Systems Taxonomy of Basic Terms(Operational World Model Ontology - Part 1
Road & Part 2: Road Users, Animals, Other
Obstacles, and Environmental Conditions)Waterloo
Intelligent
SystemsEngineering(WISE) LabJul.2018

3AVSC

AVSC Best Practice for Describing an
Operational Design Domain: Conceptual
Frameworkand Lexicon

Automated
Vehicle Safety
Consortium

Apr.2020

4OpenODD(Ontologies and ODDs at Five)(Lain Whiteside)

(Apr.
2020)

1

2

2022/2/25

NIL

12

Example (from AVSC)
The system is designed to operate on the road network in theurban center of Detroit, Michigan on all streets with a speed limitof 35mph or less. Its boundary is constrained by I-75 to thenorth; I-375 to the east; M-10 to the west; and Atwater Streetalong the Detroit River to the south. The areas around the Detroit
Police Department and Department of Public Safety are excluded
from this ODD. The system is capable of operating during daylight
hours when the sun is at or above the horizon. It can operate infair weather, including wind gusts up to 31 mph, light rain, andlight snow, provided the road surface is not covered by snow nor
standing water. It recognizes and understands all signage andtraffic control devices inside this ODD. Work zones are coordinatedwith the local transportation department and excluded from theroute network as needed. And the System needs cellularconnection.

2022/2/25

NIL

I-75
I-375

M-10
Atwater Str.

Geofence Region

13

WISE︓ODD要素• ADS for Level 4 and Level 5
Top Level

2nd Level

Top Levelroad type and capacity

ground vehicles, including their occupants

road surface type and quality
road geometry

Road structure

Road users

animal riders

cross-section designpedestrians

traffic control devices

traffic control persons

pedestrian crossing facilities

small

cycling facilities

Animalsjunctionsrailroad level crossingsbridgestunnels
driveways

medium-size
large

Other obstacles

atmospheric conditions

Environmentalconditions

lighting conditions
weather-related road surface cond.

temporary road structure2022/2/25

2nd Level

NIL

14

WISE: 例を割り当ててみる
TopLevel

Roadstructure

2nd Levelroad type and capacity

Local roads /NCroad surface type and quality

NC

road geometryNC

cross-section designNC

traffic Control devicesNC

pedestrian crossing facilities

NC

cycling facilities

NCjunctionsNC

railroad level crossingsNC

bridgesNC

tunnels-drivewaysNC

temporary road structure2022/2/25

valuesTop Level

Roadusers

AnimalsOther
obstaclesEnvironmentalconditions

NONIL

2nd Levelvalues

ground vehicles, including theiroccupantsNC

animal ridersNCpedestriansNC

traffic control persons

NC

small?

medium-size?

large?

-NC

atmospheric conditions

fair, light rain, lightsnow, no gustlighting conditions

daytimeweather-related road surface cond.

not covered bysnow
15検証可能性• 定義︓ 真或いは正しいことを証明できるという事実（the fact ofbeing able to be proved to be true or correct︔Cambridge
dictionary)• 選挙に於いては，⾃分の投票が変更されたかどうかを確認出来れば，end-toend の検証ができる
OEDR: Object and Event Detection and Response• 検証可能性: Imp (an ADS) ⊧ Spec (an ODD + fOEDR +α)• 仕様を記述することができるだろうか．できるとすれば，如何なる記述法で︖• 検証可能性を⾼める⽅法のひとつは，合理性の提⽰である．
• ひとつの例︓Toulminモデルを⽤いる
2022/2/25

NIL

16

UL4600• タイトル: 自律製品を評価するための安全性に対する標準（Standard for
Safety for the Evaluation of Autonomous Products）• 発⾏︓ 2020年4⽉• 特徴︓「論証（argumentation）」に基づくセーフティケースベース• ODD Clauses (8.2);(?)

8.2.1 運⽤設計ドメイン(ODD)は，受容可能な完全な⽅法で記述されていること

Partially
Yes ODDは，⾃律型アイテムが動作する関連する環境⾯をカバーしていること
8.2.2
NONO

8.2.3 ODDからの逸脱は，受容可能な安全な⽅法で処理されること
8.2.4 ODDの変更を検出し，解決までトレースすること

RODD
RODD+ODD
exit

RODD-RROD

2022/2/25

NIL

17

AI
MLDL

AIとプロセス•••2022/2/25

AI（⼈⼯知能）• 分類器（除く，シンボルタイプ）
ML（機械学習）• データを⽤いて，統計的に学習を⾏う• 教師あり／なし，強化学習がある
DL（深層学習）• 多数の層とノードからなり（ニューラルネットワーク），多数のデータを⽤いて，学習を⾏う
NIL

18

AIモジュールの⼀般的課題
開発• 実験管理• 限られた透明性• トラブルシューティング• リソース制約• テスト

⽣産• 依存関係の管理• 監視とログ記録• 意図しないフィードバック
ループ• グルーコードとサポートシステム

組織• 労⼒の⾒積• プライバシー• データの安全性• ⽂化の違い

Arpteg, Anders, et al. "Software engineering challenges of deep learning." 2018 44th Euromicro Conference on Software
Engineering and Advanced Applications (SEAA). IEEE, 20182022/2/25

NIL19

プロセスを考える上での考慮点
A) ライフサイクル上の位置と特性• ライフサイクルのどの位置で使⽤するかB) AIシステムのタイプ• 知識／推論／認知C) ⾞両における対象アイテムとAIモジュール• どのアイテムで使⽤しするか．その機能は．

D) 注意すべき（特有の）品質特性• ⼀般的なISO25000(SQuaRE)の前に

2022/2/25

NIL20

A）ライフサイクル上の位置と特性

Concept

Development

Pre "Type Approval(TA)"

Production

EoU

EoP

SoU

SoP

Start

［⾃律⾛⾏⾞］前提となるODD記述［AI利⽤］ データ管理プロセス／モデル管理プロセス［両者］ 型式認証後の更新，検証

Operations/Maintenance

TDecommission

Post "Type Approval(TA)"TA

Safety Update
Security Update

How to update?
How does post-type-approval realize?

How to verify?

劣化の考え⽅が異なる︓機械は経年，即ちそのモノの劣化，AIでは，環境変化に伴う不適合，モノは変化しない
2022/2/25

NIL21B)どのようなAIシステムか
出典︓Forbes, "AI Knowledge Map: How To Classify AI Technologies，⼀部のみ

https://www.forbes.com/sites/cognitiveworld/2018/08/22/ai-knowledge-map-how-to-classify-ai-technologies/?sh=7b35c5017773

コミュニケーション
計画
知識

ベイジアン
ネットワーク
ニューラルネットワーク（e.g. DL）

推論
認知

NLP／コンピュータビジョン（イメージ認識／活動認識／マシンビジョン）

確率論的⼿法2022/2/25

教師あり

教師なし

強化学習

機械学習NIL22C）どこで使⽤するか︓構造とAIモジュールの位置
ADS-DV(SAE L5)

Ic
Virtual DriverAIsLocation

Ii

Mission Planner
Route segments

Env. info

Motion Planner/Controller
Maneuvering info

Self motion info.

Trajectory Controller

Commands

Low Level Cont.

Ii

Sensor Integrator

VDIm

Id

Io
Safety Mechanism (Fallback)2022/2/25

NIL23

D）注意すべき品質特性
包括的（DIN92001），倫理上（EGTA）• 三本柱（DIN92001）• 機能／⾮機能，ロバスト性（-2，敵対／劣化），理解可能性• EGTA

EGTA カテゴリ
追跡可能性

EGTA カテゴリ
⼈間エージェンシーと監視

構成原則

透明性

コミュニケーション

⼈間エージェンシー

不公平なバイアスの除去
多様性，被差別と公平性

ステークホルダの参加

フォールバックプラン

環境負荷を上げずに継続可能である

⼀般的安全性

社会／環境の良い状態

⼈間エージェンシー

正確さ

⼈間による監視

信頼性と再⽣産性

監査可能性
説明責任

データ品質とデータの完全性個々のデータへのアクセス

2022/2/25

アクセス可能性とユニバーサルデザイン

攻撃に対するレジリエンスとセキュリティ

プライバシーとデータ保護
プライバシーとデータガバナンス

説明可能性

基本的権利
⼈間による監視

技術的ロバストネスと安全性

構成原則

悪影響の最⼩化と報告
トレードオフ救済

NIL

EGTA:=Ethics and Guidelines on Trustworthy AI (EASA)

24

AI利⽤による追加が必要なプロセス例
データ管理プロセス

EASA concept paper First usable guidance for level 1 machine learning applications• データは，これまで以上に重要な役割を果たす
データに対する要求

ラベリング
データ準備（前処理）
データ割当
2022/2/25

V&V

データ収集

–

データの正確性–

データの解像度–

注釈付きデータの品質–（通信ネットワークを介して）保存／処理／送信中の破損がないこと–

データの出所を特定する機能（トレーサビリティ）–

データが使⽤⽬的の期間に適⽤可能であるという信頼度（適時性）–

使⽤⽬的（完全性と代表性）をサポートするために必要なデータであること–

データの形式NIL

25

AI利⽤による追加が必要なプロセス例
学習管理プロセス

EASA concept paper First usable guidance for level 1 machine learning applications• 適切なモデルを採⽤すること学習に対する要求

モデル構築
学習・テストモデル
モデル評価
2022/2/25

V&V

参照モデル選択–

機能要件，⾮機能要件（WCET）–

モデルファミリとモデル選択–

学習アルゴリズムの選択–

パフォーマンスおよび安全性メトリックへのリンクを説明するコスト/損失関数の選択–モデルのバイアスと分散のメトリックおよび許容レベル–

トレーニング環境（ハードウェアおよびソフトウェア）–

モデルパラメータの初期化戦略–

ハイパーパラメータとパラメータの識別と設定–

トレーニング，検証，およびテストデータセットで期待されるパフォーマンス

NIL

26

ライフサイクルプロセスの⼀部
AIモジュール（AIM） 開発段階

#プロセス名

P.1

要求識別

P.2

学習アルゴリズム開発

P.3

学習／評価データ関連

P.4

学習

P.5

AIモジュールの評価

SCSC-153B，UL4600，DIN 92001を利⽤アイテムAIM
Model Selection and Customize, Model Creation
An appropriate algorithm type is used. (S:COM3-1)

P2(functional/non-functional)

P1

Requirements
Specificationof AIM

P2/3
Algorithm andData (S:COM1-3)

P3

Horizontal Process

Typical errors are identified
and protected against(COM3-2)
The algorithmʼs behaviour isexplainable (COM3-3)
Risk Analysis（DIN RGE）
HW/SW Separation

P2/3

Creating Training
Data (S:COM1-1,1-2)

P3.1
P3.2

ARCR
LIA

P4.1
Training

COM1-3

Acceptable Data (UL.8.5.3)

Data Evaluation (DIN 3.3)

Evaluation of Training

P5
Verification

Functional Evaluation (S:COM2-1)
Non-Functional Evaluation (S:COM2-2)
Algorithm performance is measured objectively(S:COM2-3)

Transferforoperation

Creating Verification Data

Performance boundaries are established and complied with（S:COM2-4）

AR/CR Risk Identification(DIN 5.2.2)

AR/CR Threat Model
Analysis, LIA (DIN 5.3.2)

AR/CR Robustness Evaluation（DIN:5.3.4, DIN: 5.4.4）
Test Planning（DIN: RAR_EVL.1, RCR_EVL.1）

Robustness Analysis
R: DIN 92001-2

2022/2/25

P4.2

Adversarial Robustness
Corruption RobustnessLikelihood & Impact Analysis

NIL27

プロセスに関する簡単な代数
We will consider the above in detail. Let's say design
is D and coding is C. The test is T. Abstractly, we canthink the following order.
D≺C≺T
(1)
The symbol '≺' indicates the execution order here.
Now, decompose T1 as follows.
T := T1 ≺ T2 ≺ T3

(2)

Here, T1 is test case creation, T2 is test code
creation, and T3 is test execution. Simply, (1)becomes:
D ≺ C ≺ (T1 ≺ T2 ≺ T3)(3)

However, if you think about test first, you can also:

or,D ≺ T1 ≺ T2 ≺ C ≺ T3(4)T1 ≺ D ≺ T2 ≺ C ≺ T3(5)2022/2/25

Next, consider the process instance. Now assume that {di1, di2,.., din} is an instance of process element D.
di1, ..., dik: DP1 is a critical element, and I want to confirm its
feasibility early. On the other hand, dil, ..., din: DP2 is an easy
element so that we can design it later.
If you take a strategy to tackle difficult issues first, we can get
the sequence showing below:
DP1 ≺ CP1 ≺ TP1 ≺ DP2 ≺ CP2 ≺ TP2(6)This is a kind of incremental approach. It is easy to find for us byusing parenthesis.
(DP1 ≺ CP1 ≺ TP1) ) ≺ (DP2 ≺ CP2 ≺ CP2) ≺ ...

(7)

The work products are the same in both cases. The only
difference is the choice of the process designer.
That is, the work product definition of each activity does notuniquely determine the order in which the activities are enacted.

NIL28

TM Card• 注意すべきプロセス要素を，トゥールミンモデルに従い，カード化する• 使⽤するのは，SCSC-153B，UL4600，DIN 92001
カテゴリ数

プロセスの設計DD186

QQCDWQ
DW RQ
W RW RBB
R
B
B

C

C

関連付け
C

選択

DQ
W

C

R

B

UL4600 Cards
D44

DQ

Q

設計

実装
C

DW
Q
DW R
Q
W R
W R
B
B
R
B
B

C

C

C

選択

DQ
W
B

R

C

テスト

SCSC-153B Cards
2022/2/25

NIL

29

SCSC-153A: a sample TM card
AC (Autonomous Car)

ML (Machine Learning)

D, I

COM1-1︓データは適切に取得および管理されること...完全なデータセットを取得する場合「完全なデータセットを外部から取得する場合は、「データポイズニング」の対象にならないように注意する必要があります．たとえば、悪意を持って作成されたわずかな数のサンプルがバックドアを作成する可能性があります」。 ここでは、インターネットからダウンロードした情報（チェックサムなど）の信頼性を確認するために使⽤したのと同じ⼿法が役⽴つ場合があります．

D（ML）訓練と妥当性確認のデータSo,Since

W ダウンロード時のチェックサムは同⼀であった

Q

UnlessR

たぶん(他の保証と共に)C

データポイズニン
グはない

様相論理⼦

データの管理が不⼗分であった

On account of

B ダウンロード⽅式が確⽴している

2022/2/25

Source: SCSC-153B

NIL30

まとめ
• ⾃律⾛⾏⾞の開発プロセスについて考えた．特にAIを使⽤する場合について．
• ⾃律⾛⾏⾞の前提となるのは，ODDであるが，必ずしも定まった記述法が存在するわけではない．安全性確保に強く影響する検証を困難にする原因のひとつである．
• ⾃律⾛⾏⾞もAIは，新しい技術であり，現在多くの規格を含む⽂書が発⾏され，或いは準備されている．
• さまざまな条件下で，（如何なる場合に於いても）開発プロセスを⼀意に定めることはできない．解決のためのアイデアとして，ここではTMカードについて説明した．
2022/2/25

NIL31

まとめ（将来のために）• 先に⽰した式のように，C（ODD）を導出した⽅が，正確な記述が可能となると考える．このとき，S は安全な状態であり，Pは，それを逆にCに変換する• 今の技術できることを数えると信号や標識の認識となる．しかし，重要なのは，現時点での法的制約を知ることである• 視覚優位なのは，歴史的な積み重ねに過ぎない• より確実に知る⽅法はある（⾞に対しても⼈に対しても）• 現時点では，C も P もある種の尤度を持っている．従って安全性を議論しても，ALARP を満⾜することができない
2022/2/25

NIL32

ありがとうございました

2022/2/25

NIL33