モデル・ベース開発で形式検証，自動車業界で実績上げるドイツOSC ES社の検証ツール

ドイツOSC Embedded Systems AGは，自動車の制御系設計用ツールの最大手ドイツdSPACE GmbHの日本ユーザー会で講演し，同社の検証ツール「EmbeddedValidator」について説明した。EmbeddedValidatorは，dSPACE社の自動コード生成ツール「TargetLink」向けの制御系モデルに対し，形式検証（モデル検査：model checking）を行うツールである。ある状態への到達性（reachability）解析や各種プロパティの検証，ふどうテスト・ケース生成などが可能である。 　OSC ES社の親会社はドイツOSC社で，ドイツOldenburg Universityの研究者らが1999年に設立した企業。今回の検証ツールを手掛けるOSC ES社は2002年にOSC社からスピンオフ，検証ツールを核に組み込みソフトウエアのコンサルティングなどを手掛ける。ドイツBMW社やDaimlerChrysler社，ドイツPorsche社が，既に自動車の電子制御ユニット（ECU）の開発に同社のツールを利用，日本国内では日産自動車が最大のユーザーであるという。自動車業界以外では，Airbus社などの航空機メーカーや医療機器メーカーでも採用例があるという。 　EmbeddedValidatorは，いわゆるモデル検査ツールの一種だが，モデル検査の検証エンジンは自社製ではなく，外部のものを利用している。検証エンジンは二種類あり，一つは（1）米University of California Berkeley校や米University of Texas at Austinらが開発したモデル検査ツール「VIS（verification interacting with synthesis）」，もう一つは（2）スウェーデンProver Technology ABの「Prover CL」である。前者のVISは，無償のオープンソースのツールである。 　一般にモデル検査ツールとしてはある検証項目（プロパティ）について，全ての状態空間（状態遷移パス）を調べるもの，ある一定の深さまでの状態遷移パスまでしか調べない「有界モデル検査（BMC：bounded model checking）」とがある。EmbeddedValidatorが採用するProver CLは，後者のBMC型のモデル検査エンジンである。OSC ES社 ConsultantのSven Bastrop氏によると「状態空間が大きく複雑なモデルについてはProver CLの検証エンジンを，全ての空間についてチェックしたい場合はVISを薦めている」という。