産学連携ニュース
 産学連携ニュース

デンソーが長崎県立大との自動車プロジェクトでSPARKを採用

素材
自動車
医療&健康
衣食住
環境
教育
中小ベンチャー
その他
東北地方太平洋沖地震の寄付サイト一覧
ジャストギビング(マッチング寄付)
Yahoo! 基金
GROUPON(マッチング寄付)
T-SITE(Tポイント)
mixi
GREE
モバゲータウン
アメーバピグ
記事検索
アクセスランキング トップ10










特集
お問い合わせ



あわせて読みたいブログパーツ

デンソーが長崎県立大との自動車プロジェクトでSPARKを採用

このエントリーをはてなブックマークに追加




米国のAdaCoreは、株式会社デンソー向け研究プロジェクト「Freedom from Interference(FFI)を実証するためフォーマルメソッドの適用」が成功したと発表した。

産学連携


このプロジェクトは、デンソーと長崎県立大学との共同研究で、そのゴールは、安全性が重要な自動車用アプリケーションを、自動車の電気/電子機能安全についての国際規格「ISO 26262 Road vehicles - Functional safety」に沿って開発を簡素化すること。

このプロジェクトは、レガシーなC言語コードが多くを占める自動車システムにおいて、設計方法「VDM(Vienna Development Method)」と実装言語「SPARK」を有効に使用できるか調査した。

SPARKのソフトウェアコンポーネントは、ISO 26262(FFI)の要求に従って、発生しうるレガシーCコードの妨害から保護されなければならない。

デンソーは、SPARK Proテクノロジで証明されたAdaCoreのフォーマルメソッドに関する専門的な知識と経験を評価し、AdaCoreをパートナーとして選んだ。

プロジェクトのフェーズ1ではAdaCoreと長崎県立大学はFFIの問題点についての調査を行いました。長崎県立大学のチームはフォーマルメソッドの使用について分析し、SPARKのアプローチによってシステムの安全性の検証作業を大幅に簡素化できると判断した。


統合型の静的分析ツールスイートSPARK Pro
SPARK Proはフォーマルメソッドを用いて完全性を検証する統合型の静的分析ツールスイート。「SPARK 2014」言語をサポートし、GNAT Programming Studio (GPS)ならびに GNATbench IDEに統合された先進的な検証ツールを提供する。

SPARK Proを使うことで、開発者はソフトウェアのアーキテクチャ・プロパティを形式化して定義でき、自動的にそれらを検証できる。それによって、ソフトウェアの完全性を広く保証できる。

例えば、ランタイムエラーの防止、セキュリティポリシーの強制、機能の正確性(形式化して定義された仕様に準拠していること)など。この自動検証は、ソフトウェアの障害が許容されないアプリケーションに特に適している。

SPARK Proは、コストと開発期間を削減するのを助け、フォーマルメソッドの使用によって数学的検証方法でソフトウェアライフサイクルの早い段階で問題を防ぎ、検出し、取り除く。

SPARK言語とツールは、最も要求の高いセーフティ・クリティカルかつ高セキュリティのシステムで多くの採用実績があるという。(慶尾六郎)




Amazon.co.jp : 産学連携 に関連する商品



  • 横浜ベイシェラトン ホテル&タワーズ×神奈川大学産学連携プロジェクトから、ステイプラン「感謝の旅~大切な人への贈り物~」発売(3月28日)
  • 日本システム技術×近畿大学学生起業家「やるかやらんか」、Z世代学生に向けたAIキャリアタイプ診断アプリ「MiraThin」クローズドβ版を公開(3月20日)
  • SAKURA United Solution、さくら税務実務研究所、同志社大が、税務相談AIの開発・実証実験を開始(3月11日)
  • 伊藤手帳、和歌山経済大学学生発案の留学生の気持ちに寄り添う手帳「留学DIARY」、伊藤手帳ECサイト全店で販売開始(3月2日)
  • マクロミル、データ利活用人材の創出を目指した「産学連携マーケティングリサーチ・コンテスト」を開催(2月26日)
  • Yahoo!ブックマーク  Googleブックマーク  はてなブックマーク  POOKMARKに登録  livedoorClip  del.icio.us  newsing  FC2  Technorati  ニフティクリップ  iza  Choix  Flog  Buzzurl  Twitter  GoogleBuzz
    -->
    産学連携 新着30件