形式手法は、システム構築の首尾一貫性に関する証明可能性や、実現するシステの機能安全性の観点より注目されている。我々は、リアルタイムOSに適用したシリアル通信デバイスドライバのモデルを形式手法B-Methodによる記述を試みている。昨年度までのClassical B(Atelier B)での試みに加え、並行分散システムの記述に指向したEvent-B(Rodin)を採用したので報告する。