【ET2016 プレス発表】

ソフトウェアの実行時不具合を根絶する
形式検証ツールチェーンの代理店販売開始!!
2016年11月16日
株式会社ヴィッツ
機能安全開発部
設計・技術開発室 兼 プロセス支援室 室長
水野 智仁
Copyright Witz Corporation 2016

本発表の概要• 株式会社ヴィッツは、AbsInt社（ドイツ）が開発する「ソフトウェアの実行時不具合を根絶する形式検証ツールチェーン」の代理店販売を開始しました。
• 本ツールチェーンは、従来の動的試験やシミュレーションによる検証の代わりに、論理的に正しさを立証する画期的な技術を提供します。
• これにより、品質向上、検証コスト削減を強力に支援することができます。

論理的に正しさを立証する画期的な技術
従来の動的試験やシミュレーションによる検証
Copyright Witz Corporation 20162016/11/16 ET2016プレス発表-2-

AbsInt社とツールの概要紹介【ソフトウェアの実行時不具合を根絶する形式検証ツールチェーンとは】• ツール群
ツール名
AstréeCompCert
aiT WCET Analyzers
StackAnalyzer
TimingProfiler

主な機能
ランタイムエラー解析
コードメトリックの計算
各種コーディングルールチェック
形式検証済みのコンパイラ
WCET解析
ワーストケースのスタック使用量の解析（開発初期の）WCET計測• 開発元：AbsInt社（本社：ドイツ ザールブリュッケン）• 販売実績：欧州、米国、ロシア、アジアなど– 大手自動車、航空宇宙メーカーで導入され、ツールの信頼性は証明済み
Copyright Witz Corporation 2016-3-

2016/11/16 ET2016プレス発表

背景：従来の開発における課題• 近年、様々なシステムは、複雑化が爆発しており、人手による品質確保はますます困難を極めている• 従来は膨大な動的試験を行っても、稀に不具合が発生することが、非常に大きな問題だった– 動的試験（膨大な時間とコストがかかる）• 複雑な組み合わせパターン• タイミングパターン

動的試験の問題点
正しいことを保証できない• その解決策として、形式検証によって“不具合が存在しないこと”を証明する方法が有効だと言われてきた
形式手法による検証の利点と問題点

Copyright Witz Corporation 2016

正しいことを保証できるが、高度な専門知識が必要なため、実用化されてこなかった
2016/11/16 ET2016プレス発表-4-当社の高信頼性開発のコスト削減への取り組み
2006年：機能安全の研究開発活動を開始
2008年：機能安全コンサル事業を開始
2010年：日本初 IEC 61508 SIL3 ソフトウェア開発プロセス認証を取得
2012年：世界初 ISO 26262 ASIL-D ソフトウェア開発プロセス認証を取得
2012年：開発コスト削減に注力開始【当社の開発コスト削減の主な紹介事例】
ET2014 TS-8

ET2015 TS-4

ET2016 TS-2

安全工学 Vol.54 No.6 (2015)『厳格化する安全規格！
安全設計の変貌とコスト削減策』
Copyright Witz Corporation 2016

【課題】未だ全世界においても、「低コスト開発プロセス」の決定版は無く、多大な開発・検証費を要している-5-

2016/11/16 ET2016プレス発表

当社の形式手法活用実績＆普及活動【世間の形式手法の普及状況】【当社の形式手法の実績】

海外：導入数・継続率は高く普及傾向
日本：あまり普及していない• 2006年より形式手法の研究・活用に着手。
• さまざまな形式手法の経験あり• この内、最有力となる「Bメソッド」の普及に尽力
coqisabelle

Z記法

VDM
形式仕様記述
SPIN
形式検証

SMV

Bメソッド

形式プログ
ラム合成

http://deploy-eprints.ecs.soton.ac.uk/161/2/fmsurvey%5B1%5D.pdf

CSP

SDLSCADE【課題】日本国内では、手法の利点よりも難しさが障壁に普及には、学習などの事前準備コストゼロの簡単さが必要
Copyright Witz Corporation 2016

【当社のBメソッド活用支援】• UML/SysML⇒Bメソッド変換ツール• トレーニングコース（3週間）• 活用ノウハウ集

2016/11/16 ET2016プレス発表-6-ソフトウェアの実行時不具合を根絶する
形式検証ツールチェーンの機能概要
 開発の上位工程から下位工程にわたって、検証作業を大幅に削減します。
 機能安全で要求されるツール認定作業を低減します。

Copyright Witz Corporation 2016-7-

2016/11/16 ET2016プレス発表

既存ツールの限界への改善策（1/3）
従来のツールの主な課題

本ツールチェーンによる課題の解消(A) ランタイムエラーの検知漏れ・過剰検知① ランタイムエラーを正確かつ確実に検知• 不具合の可能性は検知できるが、全ての• 形式検証技術を用いた解析によって論理不具合の検知までは保証していないため、矛盾が無いことを証明することで、不具合追加の動的検証が必要
を正確に、漏れなく検知• 正常処理に対しても、不具合の可能性として過剰に検知することがあり、これらに※某航空機メーカーの飛行制御ソフトウェア対しても確認作業が必要の解析において、過剰検知ゼロの実績あり主な課題

ツールによる確認を実施したが、検知漏れ・過剰検知があり、確認作業が大変です

課題の解消
形式検証技術で解析し、ランタイムエラーによる不具合が存在しないことを証明できます
Copyright Witz Corporation 20162016/11/16 ET2016プレス発表

過剰検知ゼロの実績があります-8-既存ツールの限界への改善策(2/3)
従来のツールの主な課題

本ツールチェーンによる課題の解消(B) 正確値ではなく推測値で最悪実行時間を算 ② 保証された最悪実行時間を算出• キャッシュとパイプライン構造の形式モデ出ルに基づき、CPUのクロックレベルで正確• 複雑なキャッシュやパイプライン構造を持つプロセッサの最悪実行時間のシナリオに最悪実行時間を算出
想定は、技術者の力量に依存• 数学的にシナリオの正しさを証明すること• 想定されるシナリオの証明、実施検証はで、タイトな時間要件の設計にも使用が可
困難
能
主な課題
最悪実行時間（WCET）に至る
シナリオは、おそらくこうだろう（推測）※確実に正しいとは言えません

課題の解消
形式モデルを使ってキャッシュとパイプラインがあるCPUでもWCETを解析できます
数学的にWCETとシナリオの正しさを保証できます
Copyright Witz Corporation 20162016/11/16 ET2016プレス発表-9-

既存ツールの限界への改善策（3/3）
従来のツールの主な課題

本ツールチェーンによる課題の解消(C) 高度な専門的知識がないと使いこなせない③ 専門的知識がなくても容易に活用できる• ソースコードまたはバイナリファイルを入• 専門的な知識を習得したエンジニアでないと使用しにくいツールのため、導入ハー力するだけの簡単な操作で、ほぼ自動的ドルが高いに解析し、結果を出力• ビジュアルに優れた高いユーザビリティを提供
課題の解消

Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 10 -

当社の今後の対応
 当社は、本製品の販売だけではなく、お客様の既存の開発プロセスとの融合を支援してまいります また、機能安全やセキュリティ開発に関する要求事項や、日本企業の開発に適した機能などを、AbsInt社に要望することにより、日本企業にとってより使いやすいツールに改善してまいります
お客様

バグなどのフィードバック
ツール販売
開発のご支援ツールの改善要望
ツールの提供Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 11 -

補足資料

Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 12 -

Astréeの機能概要①
 Astréeは、潜在的なランタイムエラーを検知するツール
 以下の潜在的なランタイムエラーを検知可能• ゼロ除算• 範囲外の配列インデックスへのアクセス• 誤ったポインタ操作と参照（NULL、未初期化、宛先がないポインタ）• 整数および浮動小数点演算オーバーフロー• 未初期化の変数への読み込みアクセス• データ競合• 一貫性のないロック（ロック／アンロック問題）• オペレーティング・システム・サービスへの無効な呼び出し• ユーザー定義されたアサーション違反• デッドコード
データ競合、一貫性のないロック（ロック／アンロック問題）、デッドロック
は、他のツールでは完全に保証できない

Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 13 -

Astréeの機能概要②
 潜在的なランタイムエラーを深刻度別に分類して報告• 形式手法に基づいた抽象解釈（abstract interpretation）によって、潜在的なランタイムエラーを100％検知し見逃さない• 深刻度別に4段階で表示可能
Cソースコードを読み込ませるだけで、ランタイムエラーを自動的に検出
深刻度
高

低

赤エラーが存在する

黄エラーは無いが、 アラームAが少なくとも1つ存在する

緑and黄

エラーとアラームAは無いが、アラームCが少なくとも1つ存在する

緑

エラーとアラームは無い

アラームA：結果が予測できない潜在的なランタイムエラー
アラームC：結果が予測可能な潜在的なランタイムエラー
エラー：
プログラムの特定の状況、条件下で限定的に発生するアラームAまたは 分析における致命的なエラー（例えば、入力ミスによる解析エラー）
Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 14 -

Astréeの機能概要③
 コーディングルールチェック静的解析ツールとして、各種コーディングルールに対応• MISRA-C:2004、MISRA-C:2012 incl. Amendment1• CWE
ユーザ独自のコーディングルール• SEI CERT C Coding Standard
チェックもオプションで用意可能• ISO/IEC TS 17961:2013• （オプション）ユーザー独自のルール

 機能安全開発におけるツール認証に必要な情報を、ユーザ様にご提供可能（ツール認証キット）
 他社の同種ツールに比べてMatlabが不要で、単体で使用可能
Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 15 -

aiT WCET Analyzersの機能概要
 aiT WCET Analyzersは、形式モデルに基づいた完全に保証できる最悪実行時間を算出するツール
 ソースコードまたは実行可能コードを入力するだけで、自動的に最悪実行時間に至るシナリオを分析、結果を出力可能
 最悪実行時間に至るシナリオと入力は、数学的に正しいことを証明可能
技術者が最悪実行時間に至るシナリオを考える必要はありません。ツールが完全保障します

Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 16 -

TimingProfilerの機能概要
 TimingProfilerは、コード開発中の動作タイミングを監視するツール
 実機を使うことなく、開発の初期段階でタイミングの振る舞いを確認できるため、ボトルネックを早期発見でき、統合時の手戻りを減らすことが可能 aiTと比べて、最悪実行時間を保証するものではないが、効果的にタイミングを推定することが可能
 グラフや表形式で関数ごとの時間情報を一覧を表示可能
 時間情報を持つコールグラフ、制御フローグラフを表示可能

Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 17 -StackAnalyzerの機能概要
 StackAnalyzerは、スタックオーバーフローが発生しないことを保障するツール
 実行可能なバイナリファイルを入力として分析が可能(デバッグ情報、計測化の技法に依存することはない) ループ、再帰、インラインアセンブリ、ライブラリ関数、Link Time
Optimizationを考慮しているので、忠実にプログラムを解析可能 安全規格に対するツール認証支援キットあり

Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 18 -

CompCertの機能概要
 CompCertは、 "machine-assisted mathematical proof"によって形式検証されたCコンパイラ
 生成されたコードが、生成元のCソースプログラムのセマンティクス(意味論)と同じ振る舞いをすることを完全保証 CompCertが生成したコードは、最適化オプションを使っていないGCCよりも2倍ほど速い速度を実現している。(ただし、レベル3で最適化されたものよりは、20％ほど速度が遅い)

Copyright Witz Corporation 20162016/11/16 ET2016プレス発表- 19 -