（全体概要）形式手法導入に伴うシステム開発過程の可視化・顕在化を通じて、システムが起こすトラブルの低減を期待すべく、我々 は、リアルタイム OS に適用したシリアル通信デバイスドライバのモデルを形式手法 B-Method による記述を試みている。 本稿では、昨年度に報告した当モデルについて、仏国の B-Method 開発ツールの会社によるコンサルティングの受講を通 じて、モデル記述に関する疑問点を解消し、種々の知見を得たので、これらを報告する。