HOME>サービス>連携検証施設「さつき」

サービス

連携検証施設「さつき」

  現在では、車、携帯電話、情報家電を筆頭に、あらゆるところに組込みソフトウェアが使用されています。その規模は年々飛躍的に増大しており、100万から1000万行といった製品も珍しくなくなってきています。その一方で、開発期間の短縮や低価格、品質向上のためにテスト量が増加しています。こうした相反する要求に応えるためには、開発プロセスの効率化は避けて通れません。

  産総研では技術相談・技術移転や共同研究の場において、モデル検査器、SAT/SMTなどの検証ツールや、Agda、VDM などの仕様記述言語を用いた開発プロセスの効率化に携わってきました。これらのツール・言語などを用いて、設計仕様が要求を満たすかの検査や、ソースコードの網羅検査、原因不明のバグの解析、テストケースの自動生成など、開発工程の上流から下流にわたってさまざまに適用し、開発の効率化を図ってきました。
モデル検査は、状態遷移モデルと検査式を与えると、モデルのあらゆる実行パスに対し、検査式を満たすかを検査する技術です。多くの静的解析ツールでは、構文情報や部分的なデーターフローに基づいて解析するので、誤検出が多かったり、検査できる内容が非常に限定的であったりします。
モデル検査は網羅的に検査するので、

  • ●一連のデータの入力系列が非常にまれな場合、
  • ●例外処理など異常系の処理、
  • ●割り込み処理、
  • ●様々なタイミングでの、並列・並行処理の切り替わり、

など、人間ではフォローしきれないまれな実行パスであっても自動で検査できます。NuSMVや Spin など、フリーソフトウェアとして提供されているものも多くあり、産総研と組込みシステム産業振興機構と共催で、こうしたモデル検査器の利用講習なども行っています。


  モデル検査はあらゆるパスを網羅的に検査するため、CPU・メモリーなど計算資源を多く必要とします。図1は、15万状態を持つプロセスをn個並行動作させた時に、バグを発見するまでにかかった時間とメモリー使用量を対数グラフで表しています。プロセス数 3までは 10Mbyte程度のメモリーで検査できましたが、この例では任意のタイミングでプロセスが切り替わるので、プロセス数5では急激に増えて、約32GByte必要となりました。実行時間もメモリー使用量に比例して増え、約1秒から約80分となっています。


  8GByte のメモリーを搭載したPCサーバーでも、モデル作成を工夫することにより、数1000行程度のC言語ソースコードに対して、多くの場合自動で検査できます。例えば、原因特定できていないバグを解析するなどの目的であれば、100万行以上のソースコードであっても、関連する部分を絞り込むことで適用可能なサイズとなり、バグ解析に大きな効果を上げることが期待できます。さらに「さつき」のクラスターであればより大規模な問題を解くことができるので、うまく数1000行に絞り込みができないなどでモデル検査できないときや、絞り込む作業時間を削減したいときなどの場合に、大きな力を発揮します。

  既に多くの企業でモデル検査等の技術を導入しています(以下敬称略)。モデル検査器SMVを使用し、上で紹介した「さつき」の利用方法で、メルコ・パワー・システムズ(株)ではバグ解析に大きな効果を挙げています。モデル検査器Spin を利用し、プリンタードライバーの未知のバグ発見に利用することや、リアルタイムシステムで優先度逆転などの問題が起こらないことを検査するなどでも、実際に使われています。また図に示すように近年、アルゴリズムの改良により飛躍的に大規模な問題に適用できるようになった SAT/SMT を利用して、テストや検証に役立てようという動きが活発化しています。例えば、インターネット上で公開されているCBMCは、YicesやCVC3などのSMTを利用して作られた有界モデル検査器のひとつです。有界モデル検査では図3のように、プログラムのパスを木で表現し、有限の深さまでを網羅的に検査します。深さに限りがあるので、それ以上の深さに誤りがあっても発見できませんが、SAT/SMTの改良によって適用可能な大きさも飛躍的に伸びています。CBMCではANSI-C言語のコードに対して、符号付整数の桁あふれや、ゼロ割、配列の境界検査、メモリーの二重開放など、さまざまな問題を自動かつ低い誤検出率で検査できます。またモデル検査と比べて、小数や多次元配列、ポインター演算を含んでいても直接扱うことができることや、nビット整数を直接表現しても性能の劣化が少ないことなどの利点があります。パナソニック(株)が開発したメモリーリーク検査器λ(ラムダ)・トレースでも、内部でCBMCを用いて検査することで、誤検出率を非常に低く抑えることができています。

   形式仕様技術やモデル検査、SAT/SMTなどの先進的な検査技術を、システム開発に広く・効果的に産業界で利用していただき、わが国の継続的な発展に寄与するために、産総研ではこうした技術導入のための教育や技術開発を行っています。さらに、連携検証施設「さつき」の所有する多種のクラスターシステムを利用し、産総研では仕様書・ソースコード等に対するモデル検査の実施を支援する検証サービスと、ネットワーク実証実験や検査技術を利用・開発するための環境を提供するサービスを、有償で実施しております。




OLS棟エントランス
OLS棟エントランス

施設外観
施設外観

検証ブース
検証ブース






連携検証施設さつき施設概要リーフレット


▲ページ先頭へ

所在地

〒563-8577 大阪府池田市緑丘1-8-31

関西産学官連携研究棟(OSL棟)

産業総合研究所 関西センター 組込みシステム技術連携研究体

アクセス

▲ページ先頭へ