【ESEC】C言語向けモデル検査ツール「CBMC」で事前・事後条件を検証，エクスモーションが実演
組み込みソフトウエア向けコンサルティングを手掛けるエクスモーションは，C言語向けのモデル検査ツール「CBMC」を用いて，C言語プログラム中の関数について事前条件・事後条件を検証する実演を見せた。関数の仕様を設計者が事前・事後条件として明示的に与えることで，関数の実装が仕様通りであることを確かめたり，関数の呼び出し関係を検証したりする。
CBMC（bounded model checking for C/C++）は，米Carnegie Mellon Universityらが開発したオープンソースの有界モデル検査ツールである（日経エレクトロニクス関連記事01）。配列の境界外アクセスやポインタのチェック，メモリ・リークの検出など主に動的なエラーの検出を得意とする。今回，エクスモーションはCBMCを，事前条件・事後条件のチェックに応用した。
通常，SPINなどのモデル検査器は，与えられた状態遷移系を総当たりですべてチェックするが，CBMCやNuSMVのような有界モデル検査器（BMC:bounded model checking）は，探索を一定の深さで打ち切るタイプの検証エンジンである（日経エレクトロニクス関連記事02）。このため特定のバグ状態がないことを保証することは原理的にできないが，単に未知のバグを検出しようとする用途には有用である。
CBMCには，「assume」や「assert」といった構文がある。assumeは事前条件として，assertは事後条件として用い，チェックしたい関数の前後に「関数の仕様」として設計者が記述する。なお，assert文は通常のC言語にも用意されているが，assume文は通常のC言語にはない構文であるため，実際にプログラムを実行する際には，assume文の行をコメント・アウトしてコンパイルする必要がある。
プログラム中のところどころにアサーションを挿入するという使い方は，一見するとCppUnitのような単体テスト・ツールに似ているように思える。しかし，行っている動作は根本的に異なる。CppUnitなどの単体テストでは，テスト対象のプログラムを実際に実行する。このため，検証できるのは，あくまで特定の実行パスにおいてアサーションが成立するかどうかだけである。これに対し，今回のようなCBMCの使い方では，設計者がテスト・ケースを与えることなく，ツール側が一定の深さまで総当たりで事前・事後条件をチェックする。
事前・事後条件は，VDMなどに代表される形式仕様記述言語に用意されていることが多い。CBMCはあくまで実装言語であるC言語が対象のため，VDMのように集合や写像を表す高度な構文を用いることはできない。しかし，「assume文の内部に関数も記述できるため，それなりのことはできる」（エクスモーション コンサルティング本部 シニアコンサルタントの藤倉俊幸氏）とする。
なお，実演を担当した藤倉俊幸氏は，形式仕様記述やモデル検査，プロセス代数，リアルタイム処理などに精通した，組み込み分野では著名なコンサルタント。2010年2月にエクスモーションに入社した。
