電子部品・デバイス

Samsung Electronics - フラッシュメモリデバイスドライバ

ドメイン
    電子部品・デバイス
開発対象
    OneNANDフラッシュメモリ
    韓国
開発組織
    Samsung、KAIST
形式手法(言語、ツール)
    BLAST, CBMC
適用範囲・規模(形式手法)
    150~2450 (LOC)
適用対象のソフト種別
    制御系
適用目的・工程
    組み込みシステムの実機テスト前
実装言語
    C
実装規模
効果
  • Samsungが過去に見つけられなかったバグを検出した。
  • セマフォ例外の不十分なハンドリング
  • 消去時の状態を保持しない論理的なバグ

(出典:Moonzoo Kim, Yunho Kim, Hotae Kim, "A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study," IEEE Transactions on Software Engineering, vol. 99, no. PrePrints, 2010 )


詳細情報

検証内容

  • OneNANDフラッシュメモリのプラットフォームソフトウェアのMSR(マルチセクターリード)の動作。
  • レースコンディションが発生しないこと
  • デッドロックが発生しないこと
  • バイナリセマフォにおいて、セマフォの数がどのステップにおいても0以上1以下であること
  • セマフォを利用している関数の動作が終了したとき、セマフォの数が1になっていること

検証規模

期間

    約6か月

判断

形式手法を利用した動機

    バグ検出

手法・ツール選択理由

  • BlastとCBMCはソフトウェアモデル検査ツールの中では安定している。(10年近くメンテナンスされている)
  • ユーザコミュニティが存在する。
  • BlastとCBMCはオープンソースソフトウェアである。検証のパフォーマンス向上等、ユーザに改善の余地が残されている。
  • 数年にわたる利用経験

障害と工夫

    フラッシュストレージプラットフォームは、物理的なユニットと論理的なユニットを結びつける複雑なデータ構造を多用するため、動作検証が難しい。

組織

体制

    Samsung Electronicsのシニアエンジニア1人の他、2人の教授、1人の大学院生が共同で開発した。

教育

その他

情報源

  • Moonzoo Kim, Yunho Kim, Hotae Kim, ""A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study,"" IEEE Transactions on Software Engineering, vol. 99, no. PrePrints, , 2010
  • Moonzoo Kim, Yunho Kim, and Hotae Kim. 2008. Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker. In Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE '08). IEEE Computer Society, Washington, DC, USA, 198-207. DOI=10.1109/ASE.2008.30 http://dx.doi.org/10.1109/ASE.2008.30
  • Moonzoo Kim, Yunja Choi, Yunho Kim, and Hotae Kim. 2008. Formal Verification of a Flash Memory Device Driver --- An Experience Report. In Proceedings of the 15th international workshop on Model Checking Software (SPIN '08), Klaus Havelund, Rupak Majumdar, and Jens Palsberg (Eds.). Springer-Verlag, Berlin, Heidelberg, 144-159. DOI=10.1007/978-3-540-85114-1_12 http://dx.doi.org/10.1007/978-3-540-85114-1_12

このページの先頭へ戻る