ディペンダブル・システムのための形式手法の実践ポータル

Microsoft - Windowsデバイスドライバ

ドメイン	その他
開発対象	126のWDM (Windows Deriver Model) ドライバと20のKMDF (Kernel Mode Driver Framework) ドライバの検証
国	米国
開発組織	Microsoft
形式手法（言語、ツール）	SLAM (Static Driver Verifier tool)
適用範囲・規模（形式手法）	WDMドライバについては60のルール（検証項目）を設定し、KMDFドライバについては40のルールを設定した。
適用対象のソフト種別	リアルタイム制御系
適用目的・工程	コード検証
実装言語	C
実装規模	48-130,000LOCであり、平均12,000LOC
効果	長年利用されてきたドライバの不具合を多数発見することができた。

（出典: Ball, T. and Bounimova, E. and Cook, B. and Levin, V. and Lichtenberg, J. and McGarvey, C. and Ondrusek, B. and Rajamani, S.K. and Ustuner, A., Thorough static analysis of device drivers, Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006）

詳細情報

検証内容

• IoCompleteRequestが呼び出されているときはドライバはSTATUS PENDINGを返さない
• もし存在するならプラグアンドプレイI/Oリクエストパケットはより低レイヤのドライバに渡される
• IoAttachDeviceToDeviceStackは適切なデバイスオブジェクトと共に呼び出される
など。

検証規模

約93%について自動的に検証することができた。

期間

判断

形式手法を利用した動機

コードが取りうる全ての振舞いを検証するため

手法・ツール選択理由

• Windowsのデバイスドライバを検証するため
• 検証のための入力を必要としないため

障害と工夫

SDVにおけるWindowsカーネルモデルやルール（検証項目）の不具合等により、デバイスドライバに不具合が無くても不具合があると報告されることがあったため、これらの修正を並行して行った。

組織

体制

教育

その他

情報源

Ball, T. and Bounimova, E. and Cook, B. and Levin, V. and Lichtenberg, J. and McGarvey, C. and Ondrusek, B. and Rajamani, S.K. and Ustuner, A., Thorough static analysis of device drivers, Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006

このページの先頭へ戻る