複雑化する車載ネットワーク、協調仕様開発で悩んだデンソーが選んだ検証方法：3DEXPERIENCE CONFERENCE JAPAN 2020 ONLINE（1/2 ページ）

[長町基，MONOist]

　ダッソー・システムズは、オンラインイベント「3DEXPERIENCE CONFERENCE JAPAN 2020 ONLINE」（2020年7月14日〜8月7日）を開催。その中でカテゴリーセッションとして、デンソー 電子PFハード開発部 ハード生産革新課の山口紘史氏が登壇し「異なる通信仕様間を制御する協調仕様の検証方法」と題して、車載ネットワークの協調仕様策定の事例について発表した。

複雑化する車載ネットワーク、使用不整合による手戻りも

　車載ネットワークにはさまざまな通信仕様が混在しており、車載ネットワークは複雑化している。異なる仕様間でも通信させるためには協調仕様が必要だが、従来は仕様の検証を、状態遷移を元にタイミングチャートを書いて検証を行っていた。複数のテストパラメータが存在するため、その数は膨大になるが、仕様開発者は経験則からテストパターンを絞り込んで検証することで何とか帳尻を合わせて開発してきた。

車載ネットワークの動向（クリックで拡大）出典：デンソー

　だが、ネットワークがより複雑になってきたことで経験則のみで対応するのが難しくなり、仕様不整合による問題がシステムテストで発覚し、大きな開発手戻りが発生する要因となっている。こうした理由から同社は「仕様設計の段階で、検証網羅性向上や仕様最適化を可能な検証手法が必要になっていた。そこでその手法構築に取り組んできた」と山口氏は語る。

新たに協調仕様の検証方法を開発した目的（クリックで拡大）出典：デンソー

異なる仕様間の不整合を素早く見つける

　新たな仕様検証の構築に向けて最も重視したことは「異なる仕様間の不整合を素早く見つけることだ。それは、不整合を解決する仕様が協調仕様となるためだ」と山口氏は述べる。まず、仕様間の不整合を検出し、次に不整合を解決する協調仕様を作成する。そして、元の仕様と協調仕様を組み合わせて検証を行う。

仕様検証手法の考え方（クリックで拡大）出典：デンソー

　同社は、検証アプローチに適した検証手法を選択するため、3つの手法を4つの指標に基づいてベンチマークテストをした。指標は検証準備期間について、モデル可読性と不完全仕様での検証可能性を仕様として挙げ、検証期間に関係する解析時間と自動証明も指標とした。手法としてはブロック図シミュレーター、形式検証、ダッソー・システムズの要求仕様検証ツールのソフトウェア「STIMULUS」を挙げて比較したが最終的に「モデル可読性、不完全仕様での検証可能性、解析時間の3つの指標が優れているSTIMULUSを選択した」と山口氏は語る。

　仕様不整合には論理的不整合とタイミング不整合の2つの不整合が起こり得る。論理的不整合は、どのようなタイミングでも仕様間の違いに伴う論理的不整合により、通信ができない状態である。送受信タイミング不整合の定義は、状態遷移のタイミングにより信号受信が不可となることをいう。

　STIMULUSはモデル内の記述内容を制約として定義し、その制約内で自由な動作を簡単にさせることができる。そのため、各仕様不整合に対するモデリングに関しては、不整合検出ルールを定義すれば、自由な動作をさせる中で、ルールを逸脱した動作を不整合として検出することができる。

　論理的不整合については各通信仕様を状態遷移図としてモデル化し、ブロック図で信号にあたる変数同士を直接接続し、異なる仕様のECU（Electronic Control Unit）間を動作できるようにし、それに対して、論理的不整合を検出するルールを定義する。一方、送受信タイミング不整合に対しては、タイミングチャートに対して、信号送信タイミングと受信可能となるタイミングのタイムラグに不整合を検出するルールを定義した。

仕様不整合に対するモデリング（クリックで拡大）出典：デンソー