2021年5月吉日

「人とくるまのテクノロジー展2021 ONLINE」出展のご案内

アイティアクセス株式会社は、5月26日（水）～7月30日（金）に開催されます

「人とくるまのテクノロジー展2021 ONLINE」
に出展することになりましたので、ここにご案内申し上げます。
今回は下記にご案内させて頂く製品群の展示を予定しております。
是非とも弊社ブースにお立ち寄りくださいますようお待ち申し上げております。

記

開催概要

【プレスリリース】

株式会社ジェイテクト、電動パワーステアリング・システム・サプライヤーが安全性重視の自動車用ソフトウエア開発にSPARK Proを採用
～SPARKの形式手法が、安全重視の自動運転システム向け開発、検証コストを削減～
[日本語] [AdaCore社サイト]

「見どころ」

Vプロセスの仕様記述からコード生成までをカバーするソフトウエア開発を支援する各種製品を紹介しています。

＊MBSE QGen　SysML_to_Simulink®  Converter（開発中）
SysMLで記述した要求図（REQ）、実装図（IBD等）をSimulinkモデルへ変換、形式検証も可能です。

＊QGen　モデルベリファイヤ＆コードジエェネレータ
Simulinkモデルの検査や形式言語を生成するコードジェネレータで　形式検証言語SPARKならびにMISRA-Cを生成することができます。

機能安全を重視した要件作成からコード生成まで対応したAdaCoreの開発環境をご覧ください。

＊SPARK Pro形式検証手法
セイフティ・クリティカルなソフトウエア開発にSPARKが応用可能でNVIDIA-SOCにも採用されました。

＊GNAT Proソフトウエア開発環境
GNAT ProはRISC-Vにも対応、多くのプロセッサをサポートする開発環境、Ada、C/C++コンパイラ、GNATstudioデバッガ、ビルダ、カバレッジツールなどが含まれています。

展示製品紹介 AdaCore社

「SPARK Pro」　状態爆発知らずの形式検証
SPARK Proは、信頼性の高いソフトウエアを開発する際にFormal Method（形式手法）を応用して検証が可能で静的解析ツールが統合された開発環境です。
プログラムは、実装部と仕様部が分けて記述し、仕様部に条件Contract（Pre/Post）を記述してソフトウエアの安全性を検証することができます。
欧米では多くの実績があり、日本でも採用が徐々に始まっています。

・特徴

■ SPARK2014（Ada)言語対応
■ 静的解析ツール
■ 非初期化変数の検出
■ ランタイムエラー検出
■ Contractベースプログラミング
■ ISO26262/IEC61508　認定

「安全認証取得」

AdaCore社は長年、安全認証を取得する上で必要なソフトウエア開発環境ならびに各種エビデンスを提供してまいりました。
＊DO-178C、IEC61508、EN50128他
GNAT Pro 開発環境、SPARK Pro形式手法開発環境で対応
＊QGenコードジェネレータは、今後DO178-C/DO331,ISO26262の安全規格を対応

「QGen モデルベリファイヤ＆コードジェネレータ」
QGenはモデルベリファイヤとコード生成を標準装備した画期的なモデルベース開発に使用できるコードジェネレータです。モデルで、静的解析を行い、ゼロ除算等の従来実行時に解析可能であったエラーを検出、開発時間を大幅短縮します。Simulink®モデルならびにStateflow®からSPARK(Ada）およびCコードを生成します。Simulink®シミュレーション結果を記録し、モデルとコードの一致性検証を行うことができます。また、QGenデバッガを併用すればモデル-C-アセンブラを同一画面で表示して実HW上でもモデルデバッグが可能です。

・特徴

■ モジュラコード生成（アップデイトされたモジュールのみコード生成）　時間の効率化
■ QGenデバッガによるモデル、C、アセンブラデバッグ
■ モデル、Cコード一致性検証対応
■ モデルベリファイヤ静的解析ツール装備
■ 生成コードを任意に変更可能
■ SPARK,Cコード生成
■ 高可読性、トレーサビリティ
■ SPARK Proと併用して形式手法開発へ応用可能
■ 認証取得用ISO26262、DO178C向けツールクオリフィケーション・キット提供
■ QGenモデルデバッガ

「GNAT Pro」

GNAT Proは、コンパイラ（Ada,C,C++)、静的解析、動的解析ツールが統合化された開発環境で、RISC-Vにも対応しています。
多くのDO-178B/C ,IEC-61508等の安全認証を取得した実績があり、認証取得用にサーティフィケーション、クオリフィケーションキットが提供されます。

【主なツール】

■ CodePeer静的解析ツール
■ GNATstack スタックチェッカ
■ GNATcoverageコードカバレッジツール
■ GNATemulator コードシミュレータ
■ 認証取得サポート
■ 認証取得用ドキュメント DO-178C、IEC61508他
■ オンサイトトレーニング
■ 開発中製品

「QGen　SysML_to_Simulink ®Converter」

SysMLで記述された図をSimulinkモデルへ変換するツールを開発中です。上位要求、アーキテクチャをSysMLで記述、変換ツールを使用して　Simulinkモデルへ変換、さらにQGenを用いてSPARKならびにCコードを生成します。そのため、コードの安全性をSPARK　 Proで形式検証可能です。ビデオにて展示しています。

上位要求からコードに至るまで一貫した開発環境がご利用可能となります。