Samsung Electronics - フラッシュメモリデバイスドライバ
ドメイン |
|
開発対象 |
|
国 |
|
開発組織 |
|
形式手法(言語、ツール) |
|
適用範囲・規模(形式手法) |
|
適用対象のソフト種別 |
|
適用目的・工程 |
|
実装言語 |
|
実装規模 |
|
効果 |
- 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になっていること
検証規模
期間
判断
形式手法を利用した動機
手法・ツール選択理由
- 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
このページの先頭へ戻る