ソフトウェアの実行時不具合を根絶する形式検証ツールチェーン

概要

本ツールチェーンでは、従来の動的試験やシミュレーションによる検証の代わりに、論理的に正しさを立証する画期的な技術を提供します。

本ツールチェーンは、AbsInt社が開発・販売しています。

  • Astrée
     
  • CompCert 
  • aiT 
  • StackAnalyzer 
  • TimingProfiler 
Astrée

Cプログラムでの全てのランタイムエラーとデータ競合の検出

Astréeは、C言語で書かれたソフトウェアプログラムでランタイムエラーとデータ競合が存在しないことを証明するために設計されたパラメトリックな静的解析ツールです。 Astréeはパラメータ化を可能とし、高精度の解析が必要とされるプログラムのために設計されています。 Astréeは、CNRS / ENSの許可を得てAbsIntによって開発され配布されています。Astréeは、航空宇宙、自動車、原子力など、さまざまな産業分野の安全重視ソフトウェアプロジェクトに使用され続けている実績があります。

Astréeの挑戦

ランタイムエラーとデータ競合は、誤ったプログラム動作を引き起こすため、ソフトウェアをクラッシュさせる可能性もあります。 ソフトウェアテストはエラーを検出する目的で使用されますが、通常、完全なテストカバレッジは不可能ですので、エラーが存在しないことまでは証明できません。 抽象解釈に基づく静的解析を使用すれば、ランタイムエラーやデータ競合が存在しないことを証明することができます。 警告の誤検知が少なければ効率的な妥当性確認プロセスに繋がります。

Astréeが検出できるエラーの例

・範囲外の配列アクセス
・誤ったポインタ操作と呼出し(NULL、初期化されていないポインタや不定なポインタなど)
・整数および浮動小数点のゼロ除算
・整数および浮動小数点の算術オーバーフロー
・未初期化変数への読み取りアクセス
・ユーザー指定のアサーション違反
・同時実行スレッド間のデータ競合
・一貫性のないロック

Astréeは、潜在的なセキュリティリスクを予防するために、 シェア変数、無限ループ、到達不能コード、MISRA-Cルール違反、CERT-CおよびCWE規約違反などもレポート可能です。

Astreeの主な特長

・Astréeは完全です。分析でエラーが検出されない場合、ランタイムエラーが存在しないことを証明します。制御とデータのカバレッジは100%です。
・Astréeは正確です。最新の分析エンジンでは、警告の誤検知率は極めてわずかです。
・Astréeには拡張性(大規模にしても費用などがそれほど増加しない)があります。 50万行を超える産業用アビオニクス(航空電子工学)ソフトウェアは、PCを使用して警告の誤検知無しに数時間で分析できました。
・Astréeは、丸め誤差を考慮した高精度の浮動小数点演算をサポートしています。
・分析対象ソフトウェアの精度調整により、警告の誤検知を安全に除去できます。
・Astréeを使用すると、分析結果を対話的に調べることができます。
・認定サポートキットが提供され、最重要レベルの自動ツール認定がサポートされます。
・AstréeはARINC653 / OSEK / AUTOSARプロジェクトのOS構成を自動考慮します。
・AstréeはdSPACE TargetLinkとシームレスに統合できますので、専用領域における最高解析精度を保証されます。

Astréeは、潜在的なセキュリティリスクを予防するために、 シェア変数、無限ループ、到達不能コード、MISRA-Cルール違反、CERT-CおよびCWE規約違反などもレポート可能です。

CompCert

形式検証された最適化Cコンパイラ

CompCertは、ミスコンパイルが存在しないことを保証するために、機械支援による数学的証明を利用する形式検証された最適化Cコンパイラです。 CompCertが生成した実行コードはCプログラムソースのセマンティクス(意味論)で特定される振る舞いとして正確に証明されます。 コンパイルプロセスの正確性が比類のない高信頼性をもたらすため、最高のソフトウェア保証レベルに寄与します。

CompCertによる印象的な出来事は、他のすべてのコンパイラで発見できなかった中程度のミスコンパイルに関するものです。 2011年初頭のCompCertの開発中バージョンはCsmithでさえ発見できなかったミスコンパイルを発見できた唯一のコンパイラでした。 この(他のすべてのコンパイラで発見できなかったという)調査が不充分であったわけではありません。 この調査に我々は延べ6CPU年時間も費やしていたのですから。 このCompCertの明からな堅牢性は、証明の枠組みにおけるコンパイラの最適化を開発することは、コンパイラユーザにとっては安全性検証というものが明示的であり機械検証可能であり、 確実な利益をもたらすものであるとする議論を巻き起こすことになりました。 (2011年のCompCertバージョンについて Regehr, Yang その他による研究

あなたの利益

・CompCert Cコンパイラを使用すれば、ソースコードレベルにおいて、 形式検証技術(静的解析、プログラム証明、モデルチェック)を適用することを自然に補完してくれます。 ソースコード上で検証されたすべての安全特性は自動的に生成された実行コード上でも保持されることが、CompCertの正確さによって保証されます。
・一般的な組み込みプロセッサー上では、CompCertによって生成された実行コードは、 最適化無しのGCCによって生成された実行コードよりも2倍の速度で実行されますし、 最適化レベル3のGCCによる実行コードよりもわずか20%遅いだけです。

可能性

・CompCertは、INRIA(フランス国立情報学自動制御研究所)のアーキテクトであり開発リーダーであるXavier Leroyの下、 多くの著名な研究者たちによるアイデアや、コードやフィードバックによって開発され続けています。
・コンパイラの証明を含むCompCertのソースコードと文書は、こちらからダウンロードできます。 研究目的に限り、CompCertを無料で利用できます。
・INRIAとAbsIntは、2014年にエンドユーザーに商用ライセンスを提供するライセンス契約について合意しました。 AbsIntは商用ライセンスを提供し、極めて強力なサポートとメンテナンスを提供し、CompCertの進歩に貢献しています。

サポート対象CPU

・PowerPC(32-bit)
・ARM
・IA32(x86 32-bit)

aiT 最悪ケースの実行時間アナライザー

リアルタイムシステムに対する時間検証

aiT 最悪ケースの実行時間アナライザーは、セーフティクリティカルシステムおけるタスクの最悪実行時間の厳密な限界値を計算します。 あらゆるシナリオやタスクの実行に際して、これらの限界値は有効かつ安全です。 aiTはタスク固有のキャッシュやパイプラインの振る舞いを静的解析しますので、 最高水準のハードウェア上の複雑で難解なリアルタイムシステムの開発が可能になります。

・aiTは、テストと測定に基づく誤りがちな手法の代わりになる、安全性を向上させる代替手法です。
・aiTは、DO-178BのレベルAまで対応した バリデーションツールとして認定されていますので、セーフティクリティカルなリアルタイムソフトウェアであることが保証されています。
・aiTは、アプリケーションの最悪ケースの実行時間の解析をサポートする自動化ツールを提供しますので、開発時間が節約できます。
・aiTは、ソフトウェアコンポーネントの相互作用のタイミングの振る舞いを決定しますので、ソフトウェアの統合が可能になります。

挑戦

・通常タスクの実行時間の測定は無害ではありません。 最大実行時間を決定するためにすべての条件を考慮していると証明することは出来ません。 なぜなら装置やツールを使用してデバッグを行えば必ずタイミングの振る舞いに影響するからです。
・キャッシュとパイプラインの振る舞いを考慮しない一般的な解析手法では、最悪ケースの実行時間を過大に見積もってしまいます。
・最悪ケースの実行時間の予測を簡略化するために、 インストラクションコードとデータキャッシュを切り離してしまえば著しいパフォーマンスの低下を引き起こしてしまいます。 (EADSの研究によると、PowerPC604では最高で30倍の退化)

これこそがaiTの出番です

・aiTの計算する限界値は、あらゆる入力値やタスクの実行に対して有効です。広範囲のタイミングテストは、もはや過去のものです。
・aiTは実行可能なバイナリを直接解析します。 そのおかげで、あなたのツールチェインを修正したり、プログラムの操作方法やパフォーマンスを修正したりする必要はなくなります。
・aiTの計算限界値は厳密ですので、あなたのシステムの実際のパフォーマンスを反映します。 キャッシュやパイプラインの影響は、完全に考慮されます。 高価なハードウェアリソースのためにデッドラインの確認を犠牲にする必要はもはやなくなりました。

aiTの機能(フィーチャー)

・アプリケーションの呼出と制御の流れの可視化。下図は、クリティカルパスと全体の最悪実行時間に対する各関数の寄与を示しています。 開発者は、最悪実行ケースのタイミングの振る舞いの最適化のに際して、関連するプログラムパーツをすばやく識別できます。
・異なるプログラムポイントにおけるマシン状態の可視化。 タイミングの最適化に際して、有効なヒントを提供してくれるパフォーマンスに影響する原因のより深い分析を開発者に与えてくれます。
・クオリフィケーションサポートキットは、 自動的なツールのクオリフィケーションを最高レベル(たとえば DO-178B, ISO-26262, IEC-61508, EN-50128 に関して) に上げるためのサポートを提供することが可能です。

なぜ、aiTが必要なのでしょう?

リアルタイムシステムの各タスクの最悪実行時間は、実行する前に知っておく必要があります。 イベントトリガー又は定周期システムでは、最悪実行時間はスケジュール解析に必要です。 つまりタイムトリガーシステム(TTA, FlexRay, ...など)に於いては、静的なスケジュールを決定する必要があります。 マイクロコントローラの性能は、シングル組み込み制御ユニットに多くの機能を実装できるほどに向上しています。 そのためソフトウェアはより複雑になり、相互作用するソフトウェアコンポーネントのタイミングの振る舞いを知ることはほとんど困難となっています。 通常はすべての潜在的な入力条件でシステムをテストすることは、実際上不可能になっています。

サポート対象プロセッサ

・PowerPC 5xx/e200(55xx, 56xx)/5777M/e300(603e, 82xx, 83xx)/750/755/7448/7447A
・i386DX
・AM486
・Motorola 68020
・ARM Cortex-M3/Cortex-R4F/Cortex-R5F (NEW)
・Infineon XMC4500(ARM Cortex-M4)(NEW)
・TI TMS320C3x
・TMS320F28
・C16x/ST10
・XC2365A-104F80L (NEW)
・HC11
・Star12/HCS12/HCS12X
・TriCore 1197/1767/1782/1784/1796/1797
・AURIX TC 275 (NEW)
・NEC/Renesas V850
・LEON2
・LEON3
・ERC32

上記以外のプロセッサに関してはお問い合わせください。

StackAnalyzer - スタック使用の分析

スタックオーバーフローは過去のものに

StackAnalyzerは、あなたのアプリケーションタスクに対して、自動的にワーストケースのスタック使用量を測定します。

なぜ、StackAnalyzerが必要なのでしょう?

スタックメモリは、プログラマによって静的に割り当てられなければなりません。 スタック使用量の過小見積もりは、スタックオーバーフローによる深刻なエラーを引き起こします。 スタック使用量の過大見積もりは、メモリリソースを浪費します。

・StackAnalyzerは、あなたのアプリケーションのスタック使用量を自動計算してくれます。分析結果は、すべての入力パラメータと各タスク実行に対して有効です。
・StackAnalyzerはバイナリー実行コードを分析しますので、デバッグ情報や装置に依存することはありません。
・インラインアセンブリコードやライブラリ関数の呼出しを考慮します。
・再帰呼出しと関数ポインタも考慮します。
・スタック使用量が表示される呼出階層グラフと制御フローグラフで自動的に可視化します。
・最新の安全規格(DO-178B/C, ISO-26262, IEC-61508, EN-50128など)では、 スタックオーバーフローが起きないことを保証することが要求されます。 StackAnalyzerは、スタックオーバーフローが存在しないことを証明できます。 AbsIntのクオリフィケーションサポートキットは、ツールのクオリフィケーションを最上位のクリティカリティレベルに設定できます。

サポートするプロセッサとコンパイラ

・C16x/XC16x/ST10 (Tasking/Keil)
・TriCore (Tasking/gcc)
・PowerPC (Diab/gcc/GHS/CodeWarrior)
・ARM (TI/ARM/gcc/GHS/Tasking/xxxxxx
・Keil MDK-ARM)
・NEC/Renesas V850 / RH850 (GHS/Diab)
・Renesas RX (IAR)
・For further targets, please contact us.
・Renesas SuperH (Renesas)
・TI C3x (TI)
・TI C28x (TI)
・TI MSP430(X) (IAR)
・x86 (gcc/ICC/cygnus)
・M68K (HP/EDS/gcc)
・FR81S (Fujitsu)
・MCS51 (TI CC254x) (IAR)
・HCS12(X/XE) (Hiware/Cosmic/IAR)
・LEON2/LEON3 (gcc/GNAT)
・ERC32 (gcc/GNAT)
・Freescale ColdFire (HP/EDS/gcc)

上記以外については、お問い合わせください。

TimingProfiler

コード開発中のタイミングの挙動を監視します

・実行時間を満たさない問題を引き起こしているアプリケーション個所を、開発者が識別することを手助けします。
・モデルベースの開発環境や、ソフトウェア開発中におけるタイミングの挙動を常時監視できます。
・コードのコンパイルと同時に結果を出力します。
・物理的なハードウェア上での測定にコストがかかる場合や、または物理的なハードウェアを用意できないような初期の開発プロセスでさえ利用可能です。

なぜ、TimingProfilerが必要なのでしょう?

・TimingProfilerは、開発の初期段階から継続的にタイミングの挙動を特定します。
・開発者は、実装の決定におけるタイミングの影響を即座に理解できます。
・TimingProfilerは、呼出し階層グラフと制御フローグラフでタイミング情報を可視化し、実行コードの関連情報を表示します。
・TimingProfilerは、開発ターゲットのプロセッサをやや理想化したモデルとして最悪ケースの実行時間評価値を計算します。 aiTと比較して、TimingProfilerはタイミングの限界値を保証するものではありませんが、タイミングの評価を計算するには有効です。
・物理的なハードウェアアクセスも、専用装置も必要ありません。
・TimingProfilerは、潜在的な入力に対するプログラム中のすべての実行パスを自動的に探索します。
・タイミング測定の準備をしたり実行したりする労力は不要です。
・TimingProfilerは、開発プロセスに簡単に統合できますから、継続的なテストと統合フレームワーク内で使用できます。
・開発者は、早期にボトルネックを識別し、終期段階での統合で生じる問題を回避できます。

サポートするプロセッサとコンパイラ

・TriCore/AURIX (Tasking/GCC)
・PowerPC (Diab/GCC/GHS/CodeWarrior)
・NEC/Renesas V850 E1, V850 E2 and RH850 (GHS/Diab)
・LEON2/LEON3 (gcc/GNAT)
・ARM (Cortex-M / Cortex-R) (TI/ARM/gcc/GHS/Tasking/Keil MDK-ARM)

上記以外のターゲットについては、お問い合わせください。

株式会社ヴィッツ

© WITZ Co.,Ltd.