ドイツOSC Embedded Systems AG（OSC ES社）は，自動車の制御系設計用ツールの最大手ドイツdSPACE GmbHの日本ユーザー会で講演し，OSC ES社の検証ツール「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を薦めている」という。
なお，自動車業界や航空機業界向けのモデル・ベース開発ツールであるフランスEsterel Technologies社の「SCADE」も，今回のEmbeddedValidatorと同じく，モデル検査エンジンとしてProver Technology社のProverを採用している。
検証したい時相論理式のテンプレートを用意
EmbeddedValidatorは，その名の通り機能要求に対してモデルの妥当性確認を行う。検証対象はdSPACE社のTargetLinkモデル，検証項目は時相論理式で記述する。ただし，時相論理式の記述に不慣れな技術者も多いため，同社のツールではあらかじめよく使う検証項目のパターンを登録した「Pattern Template Library」を用意している。論理式が成り立つ時間関係などが，グラフィカルに表示してある。
EmbeddedValidatorが対応するモデルは，現在，TargetLinkモデルだけだが，将来的にMATLAB/Simulinkの開発元である米Mathworks, Inc.の自動コード生成ツール「Real-Time Workshop Embedded Coder（RTW-EC）」向けに記述されたモデルにも対応する予定という。
OSC ES社は当初，モデル検査ツールであるEmbeddedValidatorを中心に手掛けていたが，2007年4月にはテスト・ケース生成ツール「EmbeddedTester」も投入した。また，日本の自動車メーカーへのサポートを強化するべく，日本法人を2007年に設立している。
なお，日経エレクトロニクスでは2005年12月19日号の特集記事「ソフトウエアは硬い」において，モデル検査技術や形式仕様記述などを始めとする「形式手法（フォーマル・メソッド）」について解説しております。
