国内

日立ソリューションズ - Blu-Rayディスク

ドメイン
    その他(家電)
開発対象
    Blu-Rayディスク制御ミドルウェア
    日本
開発組織
    日立ソリューションズ
形式手法(言語、ツール)
    SPIN
適用範囲・規模(形式手法)
    制御ミドルウェアの20%程度を抽象化したもの
適用対象のソフト種別
    制御系
適用目的・工程
    制御アルゴリズム検証・基本設計
実装言語
    C
実装規模
    200kLOC
効果
  • テストでは発見が困難なデッドロックの検出。
  • 制御アルゴリズムの性質の保証、想定動作の確認。
  • テスト工程半減(2ヶ月→1ヶ月)

詳細情報

検証内容

  • 要求されたディスク操作は、必ず実行され、待機状態に戻る。
  • デッドロックが存在しない。
  • モジュール間の制御状態のズレが有っても、動作停止などの問題は発生しない。

検証規模

    機能要求、安全性に関する4つの検証性質とデッドロックに関して検証した。(100%)

期間

    2008年10月~2009年3月

判断

形式手法を利用した動機

    制御の動作に関して、テストでは保証できない性質に確信を得たかった。

手法・ツール選択理由

    デバイスを含む並行システムの制御アルゴリズムの検証のためSPINが適していると判断した。

障害と工夫

  • 制御の基本設計をそのままモデリングすると並行プロセス数が多く状態爆発を発生した。
  • 抽象化のヒューリスティックスを用いて並行プロセスを減らし、対象APIを減らすことにより、APIを限定した検証が可能になった。

組織

体制

    システム分析、設計の分析は日立ソフトウェアが実施し、形式記述によるモデリングおよび検証はMRIが実施した。NTTデータ、NII、JAISTから、形式モデリングに関する助言を得た。

教育

    SPINに関する和書、洋書のテキストを5冊程度精読した。モデリング、検証作業で、オンラインマニュアルなどを利用した。

その他

    NII等からモデリングにおいて助言を得たことが効果的であった。

情報源

  • 石黒 正揮,中島 震,梅村 晃広,田中 一之、組込みソフトウェアの制御機構に対するモデル検査の適用に関する評価実験、コンピュータセキュリティシンポジウム CSS2009
  • Masaki Ishiguro, Kazuyuki Tanaka, Shin Nakajima, Akihiro Umemura, Tomoji Kishi, A Guidance and Methodology for Employing Model-Checking in Software Development, APESER: Asia-Pacific Embedded Systems Education and Research Conference, December 14-15, 2009
  • 石黒正揮,ソフトウェア開発における形式手法導入に関する課題と解決アプローチ, 先端ソフトウェア工学に関するGrace 国際シンポジウム,形式手法の産業応用ワークショップ2010,WIAFM2010: Workshop on Industrial Applications of Formal Methods, p.41-48, 2010年3月15日, 国立情報学研究所, Grace-TR-2010-03

このページの先頭へ戻る