EDA・ソフトウエア 強いLSIやボードを設計するための
 

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

進藤 智則=日経エレクトロニクス
2009/03/06 00:00
出典:日経エレクトロニクス、2005年12月19日号 、pp.113-117 (記事は執筆時の情報に基づいており、現在では異なる場合があります)
印刷用ページ

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

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

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

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

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

図7 グラフィカルにモデルを入力できるツールも登場
モデル検査を行うためには,従来は「Promela」や「SMV」などのモデル検査用の言語でモデルやプロパティを人手で作成する必要があった。現在では「Uppaal」や「SCADE」など,グラフィカルなモデルを直接入力できるモデル検査ツールが登場している。
[画像のクリックで拡大表示]

ここから先は日経テクノロジーオンライン会員の方のみ、お読みいただけます。
・会員登録済みの方は、左下の「ログイン」ボタンをクリックしてログイン完了後にご参照ください。
・会員登録がお済みでない方は、右下の会員登録ボタンをクリックして、会員登録を完了させてからご参照ください。会員登録は無料です。

<技術者塾>
電源制御と主回路の定式化手法(2日間)
~状態平均化法によるコンバータの伝達関数の導出と制御設計の基礎について事例を基にわかりやすく解説~



これまでの電源設計の教科書にはない新しい見地から基礎理論および実践例について解説するとともに、「系の安定度」の問題点と解決手法についても解説します。今年3月に発刊した「スイッチング電源制御設計の基礎」(日経BP社刊)をベースに最新の内容を解説いたします。詳細はこちら

【日時】:2015年9月28~29日 10:00~17:00 (開場9:30)予定
【会場】:化学会館(東京・御茶ノ水)
【主催】:日経エレクトロニクス

マイページ

マイページのご利用には日経テクノロジーオンラインの会員登録が必要です。

マイページでは記事のクリッピング(ブックマーク)、登録したキーワードを含む新着記事の表示(Myキーワード)、登録した連載の新着記事表示(連載ウォッチ)が利用できます。

協力メディア&
関連サイト

  • 日経エレクトロニクス
  • 日経ものづくり
  • 日経Automotive
  • 日経デジタルヘルス
  • メガソーラービジネス
  • 明日をつむぐテクノロジー
  • 新・公民連携最前線
  • 技術者塾

Follow Us

  • Facebook
  • Twitter
  • RSS

お薦めトピック

日経テクノロジーオンラインSpecial

記事ランキング