セーフティクリティカルなソフトウェアの静的解析と形式的な検証のためのユニークなツールとサービス

aiTは、バイナリファイル内のタスクによって最悪実行時間の安全で厳密な上界を算出し、対象プロセッサのキャッシュおよびパイプラインの動作を計算に入れます。TimeWeaverは、静的解析と非侵入的なトレースを組み合わせたツールです。一方、TimingProfilerを通じてソフトウェア開発の初期段階でタイミング動作を監視できます。

StackAnalyzerは、組み込みアプリケーションにおけるタスクの最悪実行スタック使用量を検出します。バイナリー実行ファイルを直接的に解析し、可能な実行をすべて計算に入れます。TargetLinkとSCADEとの緊密な統合があり、ISO 26262、DO-178B、IEC 61508などの安全標準規格に対応した認定サポートキットも利用可能です。

Astréeは、CおよびC++アプリケーションにおけるランタイムエラーや無効な並行実行が存在しないことを形式的に証明します。信頼性も速度も高く、非常に精密です。また、MISRAの準拠を検証、コードメトリクスをチェック、およびカスタムシグナルフロー、要素の干渉、サイバーセキュリティを解析できます。ISO 26262およびDO-178CレベルAの認定も可能です。

RuleCheckerは、CおよびC++コードがMISRA、CWE、AUTOSAR、その他のコーディングガイドライン、さらにはカスタムルールに準拠しているかをチェックします。また、コードメトリクスをまとめ、ISO 26262、DO-178B/C、その他の安全標準規格の認定を容易にします。さらに、TargetLink、Eclipse、µVision、Jenkinsプラグインも利用可能です。

CompCertは、セーフティクリティカルでミッションクリティカルなソフトウェア向けに形式的に検証された最適化Cコンパイラです。他のコンパイラと違って、CompCertは誤ったコンパイルが発生しないことが数学的に証明されています。このようなコンパイルプロセスの正確性への信頼は前例がなく、ソフトウェア保証の最高のレベルを満たすのに役立ちます。

Airbus Franceは20年間以上複数の航空機タイプ向けのセーフティクリティカルなアビオニクスソフトウェアの開発において、AbsIntツールを使用してきました。その中には、世界最大の旅客機であるA380の飛行制御ソフトウェアも含まれています。

本田技研工業は、ターボファンエンジンのFADECソフトウェアの開発において、AbsIntツールを使用しました。

ミュンヘン工科大学は、飛行制御およびナビゲーションアルゴリズムの開発、テスト、最適化において、AbsIntツールを使用しています。

Daimlerは、Actrosトラックの駆動系の制御システム等、多くのオートモーティブのソフトウェアプロジェクトでAbsIntツールを使用しています。

Bosch Automotive Steeringは、レガシーのツールをAstréeとRuleCheckerに置き換えました。その結果、高速な解析、高精度、そして有利なライセンス費用により、費用を大幅に削減できました。

Continentalは、エアバッグ制御システムでのスタックオーバーフローを防ぐために、長年AbsIntのスタック解析サービスを利用しています。

NASAは、2010年のトヨタ自動車の大規模リコールに対する原因調査において、タイミング関連ソフトウェア欠陥がないことを示すために、AbsIntのタイミング解析ツールを使用しました。

OHBは、静止通信衛星向けSmallGEOプラットフォームおよび衛星航法向けGALILEO FOCプラットフォームのミッションの成功に不可欠なオンボードソフトウェアの開発において、AbsIntツールを利用しています。

ESA（欧州宇宙機関）は、ジュール・ヴェルヌ自動輸送機の自動ドッキングソフトウェアにおけるランタイムエラーが存在しないことを証明するために、AbsIntランタイムエラー解析ツールを使用しました。これにより、同機が国際宇宙ステーションへ貨物を輸送することを助けました。

2003年以降、AbsIntはドイツ航空宇宙センターと8つの中期研究プロジェクトで提携しており、そのうちの1つは現在も進行中です。

2009年以降、Thales Alenia Space は5つのEU研究プロジェクトでAbsIntと提携しており、その中で、衛星通信ソフトウェアのエネルギー消費を見積もるためにAbsIntのEnergyAnalyzerというツールを使用しています。

Vestasは、風力タービン制御ソフトウェアにおけるスタックオーバーフローの防止とタイミング動作の検証するために、AbsIntツールを使用しています。

Framatomeは、原子炉の設計、テスト、運用、およびトラブル対応において使用されるセーフティクリティカルなTELEPERM XSプラットフォームを検証するために、AbsIntランタイムエラー解析およびスタック解析ツールを使用しています。

MTUは、発電所の非常用発電機向け制御ソフトウェアの正確性を確保するために、AbsIntの検証コンパイルおよび静的解析ツールを利用しています。

2000年以降、フランス原子力・代替エネルギー庁は、8つのEU研究プロジェクトでAbsIntと提携しました。その中で、1つは現在も進行中です。

組み込み無線通信および位置決定ソリューションの有力な納入業者であるu-bloxは、コンパイルの時にスタックオーバーフローを防ぎ、制御ソフトウェアの信頼性と品質を向上させるために、AbsIntツールを使用しています。

SiemensはAbsIntの専門知識を活用して、携帯電話アプリケーションのサイズを大幅に削減し、世界中の数百万台の携帯電話のフラッシュメモリに25%多くの機能を詰め込めました。