日経テクノロジーオンライン
雑誌 NEレポート

C言語を対象にしたモデル検査,富士ゼロックスがソフト検証に適用

2次不具合検証向けにC言語からPromelaへの変換器を開発

進藤 智則=日経エレクトロニクス
2009/10/15 16:00
 

C言語からPromelaへの変換器を開発し,実務に適用

 富士ゼロックスは,C言語で記述したプログラムに対して,ソフトウエアの検証技法の一つであるモデル検査を適用する技術を開発し,同社の複合機の組み込みソフトウエア開発に実際に適用した。現在の一般的なモデル検査では,専用のモデリング言語を用いて検証対象のシステムを記述し直すことが多く,この変換作業の手間がモデル検査を開発現場で実践する上での障害になっていた。今回,同社はC言語のプログラムを,モデル検査ツール「SPIN」向けの専用言語「Promela」にほぼ自動で変換するツール「FX C2P」を開発し,この手間を省いた。変換できるC言語の言語仕様に一部の制限はあるものの,専用の言語に精通していなくともモデル検査技術を用いてソフトウエアのバグの発見やデバッグなどが可能になる。

モダン・モデル検査を実用に

 モデル検査専用の言語ではなくC言語などのプログラミング言語を対象にした「モダン・モデル検査」と呼ぶモデル検査手法があり,現在,注目を集めている。FX C2Pもこの一種といえる。C言語向けのモダン・モデル検査器は,ほかにも米国の研究機関などが「FeaVer」「BLAST」といったツールを提供している。富士ゼロックスも当初,これら既存ツールの利用を検討したが,「他のツールには1パス実行の機能がなく,現場のソフトウエア技術者の視点から見て運用しにくいと感じ,内製での開発に踏み切った」(FX C2Pを開発した同社 コントローラ開発本部 コントローラプラットフォーム第二開発部の服部彰宏氏) という。

『日経エレクトロニクス』2009年10月19日号より一部掲載

10月19日号を1部買う

マイページ

マイページのご利用には日経テクノロジーオンラインの会員登録が必要です。

マイページでは記事のクリッピング(ブックマーク)、登録したキーワードを含む新着記事の表示(Myキーワード)、登録した連載の新着記事表示(連載ウォッチ)が利用できます。

協力メディア&
関連サイト

  • 日経エレクトロニクス
  • 日経ものづくり
  • 日経Automotive
  • 日経デジタルヘルス
  • メガソーラービジネス
  • 明日をつむぐテクノロジー
  • 新・公民連携最前線
  • 技術者塾

Follow Us

  • Facebook
  • Twitter
  • RSS

お薦めトピック

日経テクノロジーオンラインSpecial

記事ランキング