富士ゼロックスは，2007年1月30日から開催されたカンファレンス「ソフトウェアテストシンポジウム 2007（JaSST’07）」において，UMLを使ったモデル駆動開発（MDD）に，モデル検査（model checking）技術を適用した事例を発表した。同社は，複合機の組み込みソフトウエア開発に，MDDの一種である「Executable UML（xUML）」を使っている。モデル検査を行うには，モデル検査ツール専用の言語でモデルを作成・入力する必要があるが，同社はUMLモデルからモデル検査用のモデルを自動生成するツールを独自に開発，開発プロセスのより上流の段階でバグを見つけられるようにした。同社はこのプロセスを「Early Bird」と呼んでいる。

　富士ゼロックスは，2006年9月に開催された「第25回 ソフトウェア品質シンポジウム」にて，複合機の組み込みソフトウエアへのモデル検査の適用事例を発表している。テストでは発見が難しい非同期通信の微妙なタイミングのズレに起因するバグを，モデル検査により新規に2件発見するなどの成果を報告していた。今回のJaSSTにおける発表は，この続報という位置付けである。

　検証対象となるソフトウエア・モジュールについては，一切の抽象化をしていない。xUMLのモデルから直接，モデル検査ツール「SPIN」用の記述言語「Promela」のモデルを生成している。ただし，検証対象は複合機の一部のモジュールであるため，単体では意味のある動作をさせることができない。このため検証対象となるモジュールの外部モデルについては別途，抽象化をした上で技術者が手動で作成する必要がある。

　2006年9月の発表では，この外部モデルは，複合機の正常動作のみをモデル化していたが，今回の発表では，「紙詰まり」といった異常動作まで含めた外部モデルを手動で作成し，より広範囲な検証を実現した。現在は開発済みのモジュールに対し後からモデル検査を適用するというトライアル的な適用だが，今後，テスト技術との使い分けを明確にしながら，実際の開発プロセスに組み込めるよう工夫していくという。

　なお，今回の同社の発表は，JaSST’07の来場者による投票で決定される「ベストスピーカー賞」を受賞した。同チームは2006年9月にも，ソフトウェア品質シンポジウムにおいて最優秀論文賞を受賞しており，国内で実践例の少ないモデル検査技術の先駆けとなっている。

　同社のMDDへのモデル検査の適用については，日経エレクトロニクス 2006年10月23日号にてニュース記事として詳報しています（同記事の概要は こちら）。