| 研究概要 |
昨年度までの研究により,デバイス・ドライバが守るべき暗黙の約束事には1)関数定義の義務,2)関数の呼び出し順序の指定,3)状況に依存した関数呼び出しの義務・禁止の3種類に大別できることがわかっている.昨年度は,これらの暗黙の約束事を形式的に記述できる一種のプログラミング言語の設計を行った.本年度は,この言語の有効性の検証を行うことを目標に,いくつかのテストケースとなるデバイス・ドライバを選択し,その記述を行った.具体的にはマウス用のデバイス・ドライバ,イーサネット・カード用のデバイス・ドライバを対象に暗黙の約束事の記述を試みた.しかし,実際にデバイス・ドライバの記述をすすめてみると,関数の呼び出し順序や,状況に応じた関数呼び出しの義務および禁止を十分に記述できないことが判明した.これは,デバイス・ドライバによっては制御の流れが想定以上に複雑になる場合があり,そのような場合に記述力が十分でないことが明らかになったためである.本研究の当初の目的は,暗黙の制約を満たしているかどうかを検証可能なデバイス・ドライバ記述用言語の設計を行うことであった.しかし,実際には検証可能なような記述法でありながら,実際のデバイス・ドライバの記述に耐えるだけの表現力をもつものを実現するのは難しかった.現時点では,やや限定された表現力しかない言語で妥協し,どのような拡張を行えばよいのか検証を進めている.現在,RAMディスク用のデバイス・ドライバ程度であれば,ほぼ記述できる程度の完成度となっている.
|
