• BPnet
  • ビジネス
  • IT
  • テクノロジー
  • 医療
  • 建設・不動産
  • TRENDY
  • WOMAN
  • ショッピング
  • 転職
  • ナショジオ
  • 日経電子版

HOMEエレクトロニクス電子設計ソフトウエアは硬い > 第7回:バグをしらみつぶしに探索,仕様精査やテストの手段に(2)

ソフトウエアは硬い

第7回:バグをしらみつぶしに探索,仕様精査やテストの手段に(2)

  • 進藤 智則=日経エレクトロニクス
  • 2009/03/06 00:00
  • 1/6ページ

グラフィック入力のツールも

 モデル検査を行う際はツール内部だけでなく,使い手側の工夫も必要である。探索アルゴリズムの工夫だけで状態爆発を抑えられるわけではないため,使い手がプログラムの論理構造を抽出し,探索範囲を狭めた上で状態遷移モデルを作成する必要がある。例えば,プログラム中のループの回数を減らしたり,特定の代表値に置き換えたりする。モデル検査の適用経験が豊富なメルコ・パワー・システムズの早水氏によると,モデル作成の際「まず,わざと状態爆発するようなモデルを作成し,状態爆発の程度を見ながら徐々に絞り込んでいくのがいい」という(図6)。

図6 始めはわざと状態爆発させる
図6 始めはわざと状態爆発させる
モデル検査でモデルを作成する際は,現在のコンピュータやアルゴリズムの制約内で探索可能な状態空間に収める必要がある。ただし,その境界はつかみにくいため,始めはわざと状態爆発させ,その後,徐々に状態を絞り込んでいく。

 モデル検査ツールでは,状態遷移系を時系列に展開した際の状態遷移パスのノード数を表示する機能があり,この数の増え方があまりに急な場合は現実的な時間内に探索が終了しない。このため,ノード数の増え方がある一定のスピード以下になるまで状態空間の削減を続ける。

 なお,現在,モデル検査用の状態遷移モデルを作成する場合は「SMV」や「Promela」など各ツール専用の言語で記述する必要がある。このため,事前に状態遷移図表などを用意してあったとしても,各専用言語への変換の手間が必要となる。そこで最近では,状態遷移図表をGUIで直接入力できるモデル検査ツールも登場している(図7)。

図7 グラフィカルにモデルを入力できるツールも登場
モデル検査を行うためには,従来は「Promela」や「SMV」などのモデル検査用の言語でモデルやプロパティを人手で作成する必要があった。現在では「Uppaal」や「SCADE」など,グラフィカルなモデルを直接入力できるモデル検査ツールが登場している。
[画像のクリックで拡大表示]
【技術者塾】(8/31開催)
車載電子機器の中身はこうなっている/b>
~自動車搭載通信機(Telematics)、フル液晶クラスターパネル、衝突防止装置~


本講座では、自動車搭載通信機(Telematics)、フル液晶クラスターパネル、衝突防止装置を構成する電子部品について、実際に講師が分解した機器を見ながら解説いたします。分解の結果として、どこのどのような部品が使用され、今後はどのような機能や部品が使用されるかについての講師の考察についても述べます。市場の評価が高い、スバルのアイサイトについても解説いたします。 詳細は、こちら
日程 : 2016年8月31日
会場 : エッサム神田ホール
主催 : 日経エレクトロニクス

おすすめ ↓スクロールすると、関連記事が読めます↓