PolySpace Technologies，組み込みソフトのエラーをソース・コードから検出するツールのWindows版を販売

　フランスPolySpace Technologies社は，組み込みソフトウェアのランタイム・エラーを，プログラムを実行せずにソース・コードから検出するツール「PolySpace Verifier」のWindows版を開発した．同ツールの解析結果を表示するツールと組み合わせ，「PolySpace Developer Editon」として出荷する．

　PolySpace Verifierは，「抽象解釈」という数学的理論に基づいてソース・コードを解析し，ランタイム・エラーが発生する可能性のある箇所を検出する．ソース・コード中の命令を逐次的に解析するのではなく，取り得る値をすべて含んだ範囲（近似値）に対して解析を行う．特定の条件でしか発生しない再現性の低いエラーや，実際には実行されていない箇所についても検出できるという．検出できるエラーは，NULLポインタやポインタ境界外への不正なアクセス，配列の境界外へのアクセス，初期化していない変数の読み込み，不正な型変換，ゼロ除算や負数の平方根計算といった許可されていない計算，整数や浮動小数点数のオーバフローとアンダフロー，複数タスクから保護されていない共有グローバル変数へのアクセス，実行されないコードなど．対応言語はCとAda 83．

　PolySpace VerifierのLinux版とSolaris版はすでに発売されており，全世界で50社以上，日本国内でも10社以上が採用している（ルノー，エアバス，BMWなど）．例えば，エンジン制御やスピード制御などの組み込みソフトウェアの開発現場で使用されているという．なお，今後はLinux版とSolaris版についても，Windows版と同様に「PolySpace Developer Editon」を発売する計画．

　同社製品の日本国内での販売および技術サポートは，エーアイコーポレーションが担当している．

[写真1] PolySpace Verifier for Windowsで解析結果を表示したところ