AbsIntは組み込みシステム向けの高度な開発ツール、 およびセーフティクリティカルなソフトウェアを検証、検定、認定ためのツールを提供しています。
非公開会社のAbsIntは、 1998年に設立され、 現在は6か国出身の職員を40人以上雇用しています。この職員は、みんなドイツの本社に勤めています。
お客様は、 日本、アメリカ、カナダ、オーストラリア、そしてほぼすべてのEU加盟国を含む、世界中40か国以上に広がっています。また、アジア、北米と南米、中東、ヨーロッパにおいて、大手のソフトウェア販売代理店と協力しています。
社名の「AbsInt」は、「abstract interpretation（抽象的解釈）」に当たる略語です。 抽象的解釈とは、1977年にグルノーブルのLaboratoire d’Informatique（情報科学研究所）にて、Patrick CousotとRadhia Cousotによって形式化された高度な静的解析手法です。この手法を実施することで、当社のユニークで効果的な製品の開発が可能となりました。
事情とミッション
現在の組み込みソフトウェアの特徴は複雑性の加速度的な増加や、Time-to-market(TTM)の短縮です。セーフティクリティカルなアプリケーションの割合も増加しています。
AbsIntツールの目的：
- ソフトウェアの安全性を向上
- Time-to-market(TTM)を短縮
- テストと検証コストを削減
- ソフトウェアの効率を改善
- 組み込みリアルタイムセーフティクリティカルなアプリケーションのシステムによるコストを削減
企業紹介ビデオ
弊社のツールは生成的なフレームワークに基づいており、 顧客の ニーズに応じて迅速に、 柔軟に、 着実に対応します。 これは数多くの 成功した研究プロジェクトと、偉大な顧客満足によって証明されています。
解析・検証ツール
ソフトウェアテストは開発コストの大部分を占めています。 これは、 特に正確さは論理的な正確さだけでなく計算速度も重要なリアルタイムシステムの場合で見られます。 「タイミング プロパティを設定するのは複雑です」、 測定やタイムストッピングといった方法はエラーが発生する傾向があり、 時間もかかります。
静的解析を通じて、テストおよび検証コストを削減できます。 抽象解釈の理論に基づき、数学的に正しい解析を可能にします。これらの解析はコンパイル時に行われ、着実です。つまりあらゆるプログラム実行とあらゆる可能な入力シナリオでは結果を提供します。
リアルタイムソフトウェアのタイミング検証
賞を受賞歴したaiT WCETアナライザは、 セーフティクリティカルなアプリケーションの 対応時間を検証するための世界初の ソフトウェアツールです。 2002年以来、 aiTはAirbus Franceによってセーフティクリティカルな アビオニクスソフトウェアの タイミングを検証するために使用されています。
スタックオーバーフローが存在しないことを証明
StackAnalyzerは組込みアプリケーションにおけるタスクの 最悪スタック使用量を 自動的に算出します。 これにより開発努力が削減され、 スタックオーバーフローによるランタイムエラーの 防止に役立ちます。
ランタイムエラーが存在しないことを証明
弊社の静的解析ツールAstréeは CNRS・ENSの ライセンスの下で開発されており、CおよびC++プログラムにおけるランタイムエラーのないことを証明します。高精度かつカスタマイズできる解析エンジンにより、可能なランタイムエラーを全て検出しつつ、誤報を最小限に抑えられます。大規模な産業用安全クリティカルソフトウェアであっても、数時間以内に誤報なしで解析できます。
準拠と認定
現在の安全規格（ISO 26262、DO-178B/C、IEC-61508、EN-50125等）では、機能的および非機能的なハザードを検出し、ソフトウェアが安全目標を満たしていることを証明する必要があります。
aiT、 StackAnalyzer、 Astréeといった抽象解釈に基づくツールは、 形式的な検証による確かな結果を提供し、 認証プロセスに最適です。
さらに、弊社の 認定サポートキットを使用して、 ツールの認定プロセスを大幅に簡単にします。