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

　ドイツOSC Embedded Systems AGは，自動車の制御系設計用ツールの最大手ドイツdSPACE GmbHの日本ユーザー会で講演し，同社の検証ツール「EmbeddedValidator」について説明した。EmbeddedValidatorは，dSPACEの自動コード生成ツール「TargetLink」向けの制御系モデルに対し，形式検証（モデル検査：model checking）を行うツールである。ある状態への到達性（reachability）解析や各種プロパティの検証，オーバーフロー・チェック・テスト・ケース生成などが可能である。
→ http://techon.nikkeibp.co.jp/article/NEWS/20070625/134742/