AdaCore製品 認証取得DO-178C,EN50128,IEC61508, ISO26262 形式手法対応
| MBSE/MBD | |||
 |
SysML-Simuliink®変換
|
|
QGen コードジェネレータ QGen モデルベリファイヤ |
| 形式検証/静的解析ツール | |||
 |
形式検証 SPARK Pro |  |
静的検証ツール CODEPEER |
| 統合開発環境 Ada/C/C＋＋コンパイラ | |||
 |
GNATPRO Assurance 認証取得向け |
 |
GNAT Pro Enterprise 産業機器向け |
 |
GNAT Pro ツール |
ブログ
2021.9.2 RISC-V ISAの脆弱性
NVIDIA社は、SPARK 形式検証を使用して、安全性が重要なプログラムを開発しています。DEF CON 29会議では、ハッカーZabrocki氏とMatrosov氏が、SPARKで記述されたファームウェアに対する攻撃方法を発表しました。結論として、RISC-V ISAを攻撃することになりました。
プレス
2021.7.20 Collins Aerospaceがモデルベース開発を効率化するためにAdaCore QGenコード・ジェネレータを採用
[日本語] [AdaCore社サイト]
2020.6.24 株式会社ジェイテクト、電動パワーステアリング・システム・サプライヤーが安全性重視の自動車用ソフトウェア開発にSPARK Proを採用
～SPARKの形式手法が、安全重視の自動運転システム向け開発、検証コストを削減～
[日本語] [AdaCore社サイト]
2020.2.18 AdaCore社 Ada言語、SPARK言語、C言語対応ツールチェーン ISO 26262ならびにIEC 61508安全規格認定を取得
[日本語] [English] [AdaCore社サイト]
2019.2.15 AdaCore社はNVIDIA社と共同でファームウエアのセキュリティを強化
「Ada/SPARK言語はセキュリティ・クリティカルなソフトウェア開発と検証コストを低減」
[日本語] [AdaCore社サイト]
技術資料
モデルレベルデバッグ手法の紹介
（制御エンジニアリングとソフトウェアエンジニアリングの架け橋）
Systems-to-software integrity(SSI)：要求仕様をコードまで継承する手法のご紹介
（SysML要求仕様→Simulinkモデル→コード）
メーカー製品ページ
詳細はAdaCore社のページをご参照ください。
- AdaCore社のWEBページ
- AdaCore 資料（資料トップ）
- 書籍関連
- AdaCore 資料（日本語資料）
- AdaCore ブログ（ブログトップ）