第7回 ⾃動⾞機能安全カンファレンス 2019

テストに依存しない，ソフトウェア⽋陥を防ぐ効果的・効率的な形式検証の始め⽅〜 SPARK を⽤いて 〜
伊藤昌夫
株式会社ニルソフトウェア

⽬次
1.

課題︓⼤規模・複雑化する⾞載ソフトウェア
a.
b.

2.

⼤規模化する⾞載ソフトウェアとテスト
複雑さの増⼤︓⾃動運転⾞における安全確保の難しさ

⼀つの解決策︓テスト補完としての形式検証a.
b.

形式検証とはSPARK適⽤
i.
ii.
iii.
iv.

3.

まとめ

4.

付録

Ada ... SPARKSPARK形式検証例
なぜ，SPARKは形式検証に有利なのか
今⽇から始めるためのポータル

Reference
2019/12/5

NIL

21. 課題
⼤規模・複雑化する⾞載ソフトウェア

2019/12/5

NIL

3

⼤規模化する⾞載ソフトウェアとテスト• ⾞載ソフトウェア規模は，年々増⼤している．同⼀規模において，⼀定以上のテスト⼯数が必要となる．従ってトータルのテスト⼯数は増⼤し，如何にソフトウェアをテストするか（或いは，しないで済ますか）は，現在も今後も課題である．
規模に応じた⼀定のテスト⼯数が必要となる

幾何級数的ソフトウェア規模の増⼤（2004-2013）

中央値︓75

出典︓組込みソフトウェア開発データ⽩書 2017, IPA

出典︓Perspectives in Automotive Embedded Systems:
From manual to fully autonomous vehicles
2019/12/5

中央値︓62

NIL

4

複雑さの増⼤︓⾃動運転⾞における安全確
保の難しさ• 検証すべき様々な不確定要素が存在する
カテゴリ

ハザード

⾞両関連規格／仕様

⽋陥• ハードウェア要素の機能失陥• ソフトウェアの誤り

ISO 26262 ed.2

予定機能の誤った実⾏• センサー信号の誤った解釈・センサー
データと処理の組み合わせ誤り• HMIの誤使⽤

ISO/PAS 21448(SoTIF)

不確実さの中での状況理解• 未知の（環境）要素による安全性
侵害

N/A

複雑かつ膨⼤な動作条件を考慮に⼊れる
必要ありさまざまな対策が必要になるが ... 例えば（安全）要求の正確な記述
検証⼿段の多様化（テスト と 形式検証）
2019/12/5

NIL5

2. ⼀つの解決策
テスト補完としての形式検証

2019/12/5

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

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

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

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

- 演繹的アプローチ

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

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

2019/12/5

NIL

7

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

NIL8

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

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

証明したいこと（表明）

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

2019/12/5

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

9SPARK形式検証例︓ボディ部• 以下にボディ部における実装を⽰す．先の仕様を満⾜している必要がある．
パッケージのボディ部記述を⽰す

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

⼤きな⼊⼒値を意識し，リミット処理をしている

ボディ部︓⼿続き Increase の実装
2019/12/5

NIL

10SPARK形式検証例︓実⾏結果• 実装が仕様を満⾜しているかを確認する（メニューから，”Prove All Sources ...” を選ぶ）
• OKであれば，この⼿続きはテストが不要になる
実⾏結果
show_failed_proof_attempt.ads:8:49: medium:postcondition might fail, cannot prove X = C(e.g. when C = 0 and X = 10 and X'Old = 0)
上記メッセージの意味︓
事後条件が成⽴しない場合があります．
例えば，C=0, X = 10, XʼOld = 0 の場合です．
反例
GPS（IDE）画⾯
2019/12/5

NIL

11

なぜ，SPARKは，形式検証に有利なのか• 強い型付け⾔語Adaがベースになっており，仕様を適切に記述できる• 範囲チェックエラー,ゼロ割,オーバーフロー等は表明の記述なしに検査できる• 表明表現は，⾔語の⼀部である• 証明器を最初から開発環境に取り込んでいる
SPARK

GNATprove

VC: Verification Condition （検証条件）
SMT: Satisfiability Modulo Theories

Why3
VC

Alt-Ergo

結果
反例

結果
反例

VC

CVC4

結果
反例

VC

Z3

SMTツール群
2019/12/5

NIL

【注意】
証明できるのは，各SMTツールの能⼒の範囲においてです．
また，⾮線形の演算⼦は，通常扱うことができません．
12今⽇から始めるためのポータル
https://learn.adacore.com/オンラインコース•••••

オンライン
実⾏

Introduction to Ada
Introduction to SPARK
Ada for the C++ orJava Developer
SPARK Ada for theMISRA C Developer
Getting Started withGNAT Toolchain

2019/12/5

コミュニティ版
ダウンロードNIL

13

まとめ• ⾃動⾞に組みこまれるソフトウェアは，規模が年々増加している．今後の⾃動運転⾞の開発においては，さまざまな要素を考慮する必要があり，⾞載ソフトウェアは，より⼤規模・複雑化することが想定できる．従って，検証の負荷もますます⾼くなる．
• SPARKを⽤いることで，容易に，かつ正確に形式検証を⾏うことができ，検証に要する⼯数を⼤幅に減らすことができる．
• SPARKには，⼀貫した記述法とツール⽀援がある• もちろん，全てが形式検証可能なわけではない．しかし，⼤きな⼯数を要するテストと棲み分けすることで，トータルでコストや信頼性を向上させることが可能となる
2019/12/5

NIL

14

付録A︓SPARK応⽤例1．衛星フライトシステム
https://www.adacore.com/customers/flightsoftware-for-lunar-icecube-satellite
2．航空管制システム
https://www.adacore.com/customers/uksnext-generation-atc-system
3．Security Workstation
https://www.adacore.com/customers/multilevel-security-workstation
4．NVIDIAのSOC（ADAS・⾃動運転⾞向け）
https://www.adacore.com/press/adacoreenhances-security-critical-firmware-with-nvidia

SPARK
a anddAeverag
re to le re security.
oCadhAf twa
rks wit ages for soow
A
NVIDI ming langu
mprograhttps://blogs.nvidia.com/blog/2019/02/05/adacore-secure-

2019/12/5

NIL⽇本語要求⽂

フィードバック
フィードバック

⾃然⾔語解析

フィードバック

SPARK
コード

検査

有限状態
機械⽣成

要求⽂が明確に書かれているかを解析する
Cyclo.Req
Check

2019/12/5

15

ふるまいモデルに着⽬し，要求段階でSPARKを利⽤しているツール．要求記述・妥当性の確認を⽀援する

付録B︓Cyclo.Req
txt, docx,xlsx, pptx
(pdf)

autonomous-driving/

変換辞書

NIL

Cyclo.Req
各種検査と⽣成実際に動作させふるまい妥当性の確認を⾏う
意図通りのふるまいモデルとなっているか︖

Gen

16

Reference
1. Y. Moy, E. Ledinot, H. Delseny, V. Wiels and B. Monate, "Testingor Formal Verification: DO-178C Alternatives and IndustrialExperience," in IEEE Software, vol. 30, no. 3, pp. 50-57, MayJune 2013.
2. RTCA, Formal Methods Supplement to DO-178C and DO-278A,
RTCA DO-333, 2011.
3. D. グリース，筧 捷彦 (訳)，プログラミングの科学，培⾵館, 1991.
4. SPARK 2014 ユーザーガイド（⽇本語版）
https://www.adacore.com/uploads/techPapers/spark2014_ug.pdf

5. ⽇本 Ada 協会 https://ada.jp/

2019/12/5

NIL

17

ありがとうございました

2019/12/5

NIL

18