ランタイムエラーを静的検証のみで自動検出！

　まもなく開催されるESEC。The MathWorks／サイバネットシステムは今年、モデルベースデザイン支援ツール「MATLAB/Simulink」に加え、昨年11月に取り扱いを発表した静的検証ツール「PolySpace」を出展する。

ソースコードにエラーがないことを証明する、静的検証ツールPolySpace

　PolySpaceは、数学理論に基づく形式手法により、発見が困難な実行時（ランタイム）エラーをソースコードのコンパイル前に検証するツールだ。具体的には、ユーザーが入力したソースコードに対し、変数の値をトレースして演算の正しさを判別。その結果を4色に分類（正常 ／必ずエラーが発生する／実行されない ／場合によってはエラーが発生する）して表示する。

サイバネット 応用システム第1事業部 技術部 アドバンストサポート第2グループ 渡辺 繁氏

　関数・ファイル間に渡る制御フローに沿って変数の値を追跡し、検査対象となる各演算の“正しさ”を漏れ（偽陰性）なく網羅的に検証している。テストケースを作成しなくても、実行時エラーが検出でき、同時にエラーが存在しないことも確認できる。

　つまり、「一般的な静的解析ツールがバグ（エラー）を見つけるものだとすれば、PolySpaceはバグが1つもない（ゼロである）ことを証明するツール」――と担当者の渡辺氏（サイバネットシステム）が語るように、これまでの静的・動的ツールでは難しかったソースコードに実行時エラーが潜在しない信頼性の確認を、静的検証のみで行うことを可能にしたのがPolySpaceだ。

画像1 PolySpaceでの表示例 演算の正しさを判別することで、コードの信頼性を測定する。4色の配分はグリーン・レッド・グレー・オレンジで、それぞれ「正常」「必ずエラーが発生する」「実行されない」「場合によってはエラーが発生する」

　検出される実行時エラーとは、コンパイル時には検出されずにプログラム実行中に発生するソフトウェアの致命的な不具合のことで、PolySpaceでは主に以下のエラーがそれに当たる。実行時エラーは、まれにしか発生せず、また再現性の乏しいことから、テストでの発見は難しいとされている。ただし、一度起こるとメモリ破壊や暴走を引き起こし、もし出荷後に発生すると、リコールなどの多大な損害が発生してしまうため早期発見が求められている。

　サイバネットシステムの展示ブースでは、上記のエラーを含むサンプルコードを基に、実際にPolySpaceを使用した検証結果を確認できるという。

画像2 PolySpaceの運用イメージ 複数のユーザーが複数のPolySpaceクライアントからコンピュータクラスタ上のPolySpaceサーバを使用するイメージ。各検証ジョブは実行可能なサーバに送信され、そこで実行された検証結果をクライアントからダウンロードできる

　高い信頼性が求められる組み込みソフトウェア開発の現場では、実行時エラーを除くためにテストケースの作成やレビューなどに多大なコスト・時間が費やされているのが現状だ。テストケースの作成も不要で、実行時エラーを確認できるPolySpaceの操作性を会場で試してみてはいかがだろうか。

MATLAB/Simulinkとの連携も

　さらに、PolySpaceはMATLAB/Simulinkとの連携も可能にしている。モデルから生成したソースコードのPolySpaceの検証結果からモデル側の該当箇所へリンクし、コードの設計仕様であるモデルの問題を確認でき、より早期段階で問題点を修正できる。

画像3 モデルベースデザイン用アドオンによる連携画面

◇

　なお、会場では、実行時エラー当てクイズの簡単な催しも予定されているとのこと。