以下のウェビナーを見落とし方へYouTubeに本ウェビナーの録画をアップロードしております。ご登録の上、ぜひご覧ください。

ウェビナー

形式検証手法を用いてソフトウェアの安全性、信頼性を向上、JTEKTの電動パワステへの形式検証SPARK Pro応用事例のご紹介

概要

自動運転技術の導入が進む自動車に搭載されるソフトウェアは増大の一途をたどっており、加えてより高い安全性、信頼性の確保が要求されています。そのため、開発スケジュールを順守しつつ、より高い品質を達成することが重要になります。そこで、ソフトウェア開発の早い段階で欠陥を確実に発見でき、テスト工数、手戻りを減らすことが可能な開発手法として形式検証を応用した事例をご紹介します。

本ウェビナーでは、株式会社ジェイテクトが、電動パワステへの形式検証SPARK Proを応用した事例を、実例を示しながら紹介します。

こんな人にオススメ
･ 高い信頼性、安全性が要求されるソフトウェアを開発される方
･ ソフトウェアのテスト工数を削減し、手戻りを少なくする手法を検討している方
･ ハードウェアの制約などで、ソフトウェアテストに苦労されている方
･ 形式検証を検討されている、ご興味のある方

【セミナー詳細】

【お申込に関して】
お申込ページ

【個人情報に関して】
・ご登録いただいた情報は、アイティアクセス株式会社にて厳正に管理されます。 ご記入された「お客様の個人情報」の取り扱いはアイティアクセス株式会社の個人情報保護方針に従うものとします。お客様の許可なく第三者に開示されることはございません。詳細についてはhttps://www.itaccess.co.jp/privacy/をご覧ください。
・お申込ページにてお客様にご同意いただいた場合、ご記入された「お客様の個人情報」は主催のAdaCore社に提供させていただきます。

プレスリリースのご案内

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

AdaCore社について

1994年に設立されたAdaCore社は、ミッション・クリティカル、セーフティ・クリティカル、かつセキュリティ・クリティカルなシステム向けにソフトウェア開発・検証ツールを提供しています。主力商品は次の4つです。
･ GNAT Proは、Ada、C、C++に対応した統合化開発環境で、高い信頼性と保守性が要求されるアプリケーションを、設計、実装、管理する為のツールセットです。
･ CodePeerは、CWE準拠の先進的なAdaコード用静的解析ツールで、ソフトウェアのエラーを検出し、レビューして検証する機能を備えています。また、CodePeerは、MITRE社のCommon Weakness Enumeration（CWE）で「最も危険なソフトウェアエラー上位25」の検出が可能です。
･ SPARK Proは、形式検証をベースに、高信頼性システムの開発に適した検証環境です。
･ QGenは、DO178Cツール資格を取得する等、セーフティが重要な制御システム向け、モデルベース開発ツールスイートで、Simulink®およびStateflow®モデルの静的な検証ツール、コード・ジェネレータ、さらにモデルレベルのデバッガを提供します。

長年にわたり、AdaCore社製品ご利用のお客様は、セーフティ・クリティカルなアプリケーションを開発し、保守を継続しています。その分野は、商用航空機、自動車、鉄道、宇宙、軍事、航空交通管制、医療機器、財務サービスなどです。AdaCore社の顧客は、世界的に幅広い分野で増え続けています。詳細については、https://www.adacore.com/industries　（英語）をご覧ください。

アイティアクセス株式会社のAdaCore製品サイトは以下を参照してください。
https://www.itaccess.co.jp/service/adv/brand/adacore/