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

デンソーが長崎県立大との自動車プロジェクトで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 : 産学連携 に関連する商品



  • 東京都市大と理研など、軽量化を可能にする新鋼材開発法を開発(2月15日)
  • 白銅、東京理科大、キヤノンMJが金属3Dプリンター材料を共同開発(2月15日)
  • 産学連携を効果的にする人工知能ナレッジマネジメントシステム(1月31日)
  • 東大と慶大らが空間を飛び回るLED光源を開発(1月19日)
  • ソラシドエアとバンタンのプロジェクト公認キャラクター決定(12月27日)
  • Yahoo!ブックマーク  Googleブックマーク  はてなブックマーク  POOKMARKに登録  livedoorClip  del.icio.us  newsing  FC2  Technorati  ニフティクリップ  iza  Choix  Flog  Buzzurl  Twitter  GoogleBuzz
    -->
    産学連携 新着30件