コードの安全性を確保する
各ステップを見ていきましょう。

Astrée — static runtime error analysis
►

Astréeを使ってCまたはC++コードにおけるランタイムエラーを検出できます。

ゼロ除算、配列の境界外アクセス、誤ったポインタ操作、算術オーバーフローをすべて検出します。データ競合、誤ったロック、その他の種類のエラーも検出できます。解析を簡単に設定して、ビルドプロセスの一部として自動的に実行します。

↓
RuleChecker — automatic checks for adherence to coding standards
►

RuleCheckerを使ってコーディングガイドラインを検証できます。

CまたはC++コードを、MISRA、CWE、SEI CERT、ISO/IEC、AUTOSARのガイドライン、さらに社内のコーディングルールへの準拠をチェックします。必要に応じて、ルールを簡単にトグルしたりカスタマイズしたりできます。コメント率や循環的複雑度などのコードメトリクスを監視し、ドキュメンテーションや認証のためのレポートを生成します。

↓
CompCert — verified compilation
►

CompCertを使ってコードをコンパイルできます。

ソフトウェア保証の最高レベルを実現するには、誤ったコンパイルの問題がないことが形式的に検証された唯一のCコンパイラでアプリケーションをコンパイルします。例えば、Astréeを使用してソースコードで検証したすセーフティプロパティが、生成された実行ファイルでも確実に保持されます。

↓
StackAnalyzer — static stack-usage analysis
►

StackAnalyzerを使ってスタック使用量をチェックしましょう。

アプリケーション内のタスクの最悪スタック使用量を計算します。スタックオーバーフローを検出するか、その不在を形式的に証明します。クリティカルセクションや実行経路を迅速に特定して、コードのパフォーマンスを最適化します。

↓
►

aiT、TimeWeaver、TimingProfilerで実行時間を解析しましょう。

aiT — static timing analysis

aiT WCET Analyzers

バイナリ実行ファイル内のタスクにおける最悪実行時間の厳密な上界を算出します。テストや測定は不要です。静的解析によって、算出された上界があらゆる実行経路、すべての入力の組み合わせ、キャッシュやパイプラインの状態に対して保証されます。

TimeWeaver — hybrid WCET analysis based on execution traces

TimeWeaver

プロセッサが複雑すぎて設計できない場合でも、リアルタイム命令レベルのトレースデータから得られるタイミング測定と静的な経路解析を組み合わせることで、静的解析が提供する効率性と安全性を活用できます。

TimingProfiler — exploring timing effects at early design stages

TimingProfiler

ソフトウェア開発の初期段階から、タイミング動作を継続的に監視します。プロセッサが未選定の段階や、ハードウェアでの測定が不可能な場合でも、ボトルネックを特定できます。

↓
Qualification support
►

ISO 26262、DO-178B/C、IEC-61508、EN-50128、 FDA等の準拠。

認定サポートキットおよび認定ソフトウェアライフサイクルデータレポートを使用して、資格取得の過程を簡単で自動化します。