C言語からPromelaへの変換器を開発し，実務に適用
富士ゼロックスは，C言語で記述したプログラムに対して，ソフトウエアの検証技法の一つであるモデル検査を適用する技術を開発し，同社の複合機の組み込みソフトウエア開発に実際に適用した。現在の一般的なモデル検査では，専用のモデリング言語を用いて検証対象のシステムを記述し直すことが多く，この変換作業の手間がモデル検査を開発現場で実践する上での障害になっていた。今回，同社はC言語のプログラムを，モデル検査ツール「SPIN」向けの専用言語「Promela」にほぼ自動で変換するツール「FX C2P」を開発し，この手間を省いた。変換できるC言語の言語仕様に一部の制限はあるものの，専用の言語に精通していなくともモデル検査技術を用いてソフトウエアのバグの発見やデバッグなどが可能になる。
モダン・モデル検査を実用に
モデル検査専用の言語ではなくC言語などのプログラミング言語を対象にした「モダン・モデル検査」と呼ぶモデル検査手法があり，現在，注目を集めている。FX C2Pもこの一種といえる。C言語向けのモダン・モデル検査器は，ほかにも米国の研究機関などが「FeaVer」「BLAST」といったツールを提供している。富士ゼロックスも当初，これら既存ツールの利用を検討したが，「他のツールには1パス実行の機能がなく，現場のソフトウエア技術者の視点から見て運用しにくいと感じ，内製での開発に踏み切った」（FX C2Pを開発した同社 コントローラ開発本部 コントローラプラットフォーム第二開発部の服部彰宏氏） という。
『日経エレクトロニクス』2009年10月19日号より一部掲載
