PR

ドイツ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を薦めている」という。

この記事は会員登録で続きをご覧いただけます

日経クロステック登録会員になると…

新着が分かるメールマガジンが届く
キーワード登録、連載フォローが便利

さらに、有料会員に申し込むとすべての記事が読み放題に!
有料会員と登録会員の違い


日経クロステックからのお薦め

車載Ethernetセミナー2021

車載Ethernetセミナー2021

次世代の車載ネットワークの最新動向をオンラインセミナーで解説

トヨタ、ホンダ、BMW、デンソー、コンチネンタルなど、国内外の講師を招聘、毎年人気のイベントを今年も開催。

詳しいプログラム、お申し込みはこちら

『アカン!DX』

『アカン!DX』

日本企業と行政のDXの隠れた大問題を見える化!

DXブームは既に腐り始めている――。人気コラム「極言暴論」「極言正論」の筆者が、日本企業や行政のDXの問題点をずばり指摘する。経営者から技術者までDXに取り組むすべての人の必読書!

書籍『アカン!DX』の詳細はこちら

IT/電機/自動車/建設/不動産の編集記者を募集します

IT/電機/自動車/建設/不動産の編集記者を募集します

“特等席”から未来づくりの最前線を追う仕事です

あなたの専門知識や経験を生かして、「日経クロステック」の記事や書籍の企画、取材・執筆・編集を担う編集記者(正社員)にトライしませんか。編集の経験は問いません。コミュニケーション能力が高く、企画力や実行力があり、好奇心旺盛な方を求めています。

詳しい情報を見る

日経BPはエンジニアや企画・営業も募集中