お知らせ

News

ご挨拶

「自動車機能安全カンファレンス」デモ出展 およびAdaCore社来日講演のご案内


アイティアクセス株式会社

2018年11月吉日

「自動車機能安全カンファレンス」出展のご案内

アイティアクセス株式会社は、12月6日(木)~12月7日(金)御茶ノ水ソラシティカンファレンスセンターにおきまして開催されます「自動車機能安全カンファレンス」に出展することになりましたので、ここにご案内申し上げます。
是非とも弊社ブースにお立ち寄りくださいますようお待ち申し上げております。

開催概要

■名称 「自動車機能安全カンファレンス」
■会期 12月6日(木)~12月7日(金)
■会場 御茶ノ水ソラシティカンファレンスセンター
■セミナー 10:00-18:00(最終日17:20まで)
■入場料 無料(事前登録)
■主催 株式会社インプレス
■共催 一般財団法人日本自動車研究所(JARI)

 

「見どころ」

Vプロセスの仕様からコード生成までをカバーする製品の展示ならびに自動運転制御システムの安全監視(RTA)ソリューションをセミナーでご紹介します。

 

「セミナー」

AdaCore社から形式手法の開発を担当するヨハネス・カニグ博士が来日して講演を行います。

講演タイトル:形式検証を応用した自動運転プログラムの安全確保手法
講演日時:12月6日(木)15:35~15:55(A2-2)

講演概要:SPARKPro形式検証手法は、長年、航空宇宙等の高信頼性ソフトウエアを搭載した機器で利用されています。
プログラムの確からしさを検証後、コンパイルして実機で動作可能です。
その技術をAI等で構成される自動運転(レベル4)プログラムの監視システムへ応用し、安全性を確保する手法を紹介します。

 

「展示」

以下の製品をパネルあるいはビデオでご紹介いたします。

*RTA(Run Time Assurance)
RTAは、自動運転制御システムにおいて、車両の挙動をセンサーから報告される状態の監視を行い、不正な挙動が検出された場合、バックアップシステムへ切り替え、安定した運転制御が継続出来るように支援します。
*SysML_to_Simulinkモデルコンバータ
SysMLで記述した要件、図をSimulinkモデルならびにC,SPARKコードへ変換するツール(開発中)
*QGen Verifier&CodeGenerator
Simulinkモデルの検査や形式言語を生成するコードジェネレータを用いて形式手法検証を行うことができます。

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

*仕様書検査(日本語対応)Cyclo.Req
日本語表記の仕様書を検査して目的語が無い等の誤りを訂正、SPARK言語を生成して仕様の振舞検査が可能なツール。

展示製品紹介 AdaCore社

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

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

特徴

  • DO333認証取得予定
  • SPARK2014(Ada)言語対応
  • Contractベースプログラミング
  • 静的解析ツール対応

「安全認証取得」

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

*DO-178C、IEC61508、EN50128他

GNATpro 開発環境、SPARKpro形式手法開発環境で対応

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

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

QGenはモデルベリファイヤとコード生成を標準装備した画期的なモデルベース開発に使用できるコードジェネレータです。
モデルを未コンパイルで、静的解析を行い、ゼロ除算等の従来実行時に解析可能であったエラーを検出、開発時間を大幅短縮します。

SimulinkモデルならびにStateflowに対応し、SPARK(Ada)およびCコードを生成します。Simulinkシミュレーション結果を記録してCレベルにて一致性検証を行うこともできます。
また、QGenデバッガを併用すればモデル-C-アセンブラを同一画面で表示して実HW上でモデルデバッグが可能。

特徴

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

QGenモデルデバッガ

 

「GNATpro」

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

主なツール

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

認証取得サポート

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

開発中製品

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

SysMLで記述された図をSimulinkモデルへ変換するツールを開発中です。上位要求、アーキテクチャをSysMLで記述、変換ツールを使用して SimulinkモデルあるいはC/SPARK言語へ変換します。そのため、形式検証を行いコードの安全性、セキュアであることがSPARKProを用いて検証可能です。

 

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

展示製品紹介 Nil社

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

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

お問合せ先

アイティアクセス株式会社 事務局担当
【新横浜本社】
〒222-0033 横浜市港北区新横浜3-17-6
TEL : 045-474-9095 / FAX : 045-474-8823
【大阪オフィス】
〒541-0054 大阪府大阪市中央区南本町2-6-12
サンマリオンNBFタワー 16階
TEL : 06-6121-8005 / FAX : 06-6121-8038E-mail : info@itaccess.co.jp
URL : https://www.itaccess.co.jp/
PAGE TOP