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

国内

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

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

2008年10月～2009年3月

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

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

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

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

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
石黒正揮,ソフトウェア開発における形式手法導入に関する課題と解決アプローチ, 先端ソフトウェア工学に関するＧｒａce 国際シンポジウム,形式手法の産業応用ワークショップ2010,WIAFM2010: Workshop on Industrial Applications of Formal Methods, p.41-48, 2010年3月15日, 国立情報学研究所, Grace-TR-2010-03