2019年9月吉日

「[名古屋]カーエレクトロニクス技術展」出展のご案内

アイティアクセス株式会社は、9月18日（水）～9月20日（金）ポートメッセ なごやにおきまして開催されます「[名古屋]カーエレクトロニクス技術展」に出展することになりましたので、ここにご案内申し上げます。
今回は下記にご案内させて頂く製品群の展示を予定しております。
是非とも弊社ブースにお立ち寄りくださいますようお待ち申し上げております。

記

開催概要

■名称	「[名古屋]カーエレクトロニクス技術展」
■会期	9月18日（水）～9月20日（金）
■会場	ポートメッセ なごや
■小間番号	5-30
■入館時間	10：00-18：00（最終日のみ17時まで）
■入場料	無料(事前登録)
■主催	リード エグジビション ジャパン(株)

 

プレスリリース

＊～AdaCore社はNVIDIA社と共同でファームウエアのセキュリティを強化～
「Ada/SPARK言語はセキュリティ・クリティカルなソフトウエア開発と検証コストを低減」

＊～AdaCore社はRISC-V財団に加盟C/Adaコンパイラを提供開始～
「GNAT ProとGNATコミュニティのツールチェーンが業務用とホビイスト用両方で利用可能」

「見どころ」

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

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

＊QGen　Verifier&CodeGenerator
Simulinkモデルの検査や形式言語を生成するコードジェネレータを用いて形式手法検証を行うことができます。

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

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

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

展示製品紹介 AdaCore社

「SPARK Pro」　状態爆発知らずの形式検証

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

特徴

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

「安全認証取得」

AdaCore社は長年、安全認証を取得する上で必要なソフトウエア開発環境ならびに各種エビデンスを提供してまいりました

＊DO-178C、IEC61508、EN50128他

GNATpro 開発環境、SPARKｐro形式手法開発環境で対応

＊QGenコードジェネレータでは、今後DO178C/DO331,ISO26262の安全規格を取得いたします。

「QGen モデル・ベリファイヤ＆コードジエネレータ」

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

特徴

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

QGenモデルデバッガ

 

「GNATpro」

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

主なツール

• CodePeer静的解析ツール
• GNATstack スタックチェッカ
• GNATcoverageコードカバレッジツール
• GNATemulator コードシミュレータ

認証取得サポート

• 認証取得用ドキュメント DO-178C、IEC61508他
• オンサイトトレーニング

開発中製品

「SysML-Simulink モデルコンバータ」

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

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

展示製品紹介 Nil社

「Cyclo.Req 日本語仕様書解析ツール」

Cyclo.Reqは、日本語で記述された仕様書を検査しその曖昧さを示します。である/.ですますはもとより文の長さ、目的語の欠落、係り受けの長さ等の検査が可能です。係り受けに関しては図示して、文書を変更するのに役立ちます。
また、日本語検査が終了した仕様書からFSM(有限状態機械）ならびにSPARK言語を生成、コンパイルして振舞検査を実できるため、仕様書の矛盾も検出可能です。