富士ゼロックスは,ソフトウエアの振る舞いを網羅的に検証する手法として注目を集めている「モデル検査」を,同社の複合機「ApeosPort」シリーズの組み込みソフトウエア開発に適用した。現在,ソフトウエアの品質確保で主体となっているソフトウエア・テストでは発見が難しい,微妙なタイミングに起因するバグを2件検出するなど先駆的な成果を上げた。2006年9月に開催されたソフトウエア関連の学会で明らかにした。

 対象としたのは,ApeosPortに向けた約1000万行のソフトウエアのうち,「インタフェース・マネジャー」と呼ぶ約6万行のモジュールである。今後発売する機種に適用する。モデル検査ツールとしてはオープン・ソースの「SPIN」を用いた。「単純な比較は難しいが,今回発見したバグを通常のテストで検出しようとすると,恐らく数千項目以上のテスト・ケース,500人・日程度のテスト実施工数を要する。これを数分の検証時間で検出できた。非常に大きな効率向上だ」(取り組みを主導した同社 オフィスプロダクト事業本部 コントローラーソフトウェア開発部の服部彰宏氏と山本訓稔氏)。