ポリスペース

ポリスペース
開発者マスワークス[ 1 ]
安定版リリース
R2022b / 2022年9月15日 ( 2022-09-15 )
オペレーティング·システムクロスプラットフォーム[ 2 ]
タイプ静的コード分析
ライセンス独自の
Webサイトwww.mathworks.com/products/polyspace.html ウィキデータで編集する

Polyspaceは、 CC++Adaプログラミング言語のソースコードにおける特定の実行時エラーを検出、または存在しないことを証明するための、抽象解釈による大規模解析のための静的コード解析ツールです。また、ソースコードが適切なコード標準に準拠しているかどうかもチェックします。[ 3 ]

歴史

PolyspaceはもともとフランスのPolySpace Technologies社によって開発され、同社は2007年にMathWorks社に買収されました。[ 4 ]その後、この製品はMATLABに統合されました。

一般的な用途

Polyspaceはソースコードを検査し、算術オーバーフローバッファオーバーランゼロ除算などの潜在的な実行時エラーが発生する可能性のある箇所を特定します。ソフトウェア開発者や品質保証マネージャーは、この情報を使用して、コードのどの部分に欠陥があり、どの部分に信頼性が実証されているかを特定します。コードのその他の部分は未検証チェックとしてマークされ、個別にレビューする必要があります。[ 5 ] [ 6 ]

MISRA Cなどのコード標準やガイドラインは、コードの品質、移植性、信頼性に焦点を当てています。本製品は、CおよびC++のソースコードがこれらのコーディング標準の規則のサブセットに準拠しているかどうかを検査します。[ 7 ]

機能

この製品ファミリーは、Polyspace Code ProverとPolyspace Bug Finderで構成されています。Code Proverモジュールは、ソースコードに色分けされた注釈を付け、コード内の各要素の状態を示します。[ 8 ]形式手法に基づく静的コード解析を用いて、言語レベルでプログラムの実行を検証します。[ 6 ]このツールは、コード内のあらゆるポイントですべての変数のすべての可能な値を考慮して各コード命令をチェックし、通常の使用状況と異常な使用状況の両方において、コード内の各操作について正式な診断を提供します。[ 9 ]

Bug Finderモジュールは、ソースコードに対して静的プログラム解析を実行することで、ソフトウェアのバグを特定します。数値計算、プログラミング、メモリ、その他のエラーなどの欠陥を検出します。また、ソースファイルのコメント密度、循環的複雑度、関数の行数、パラメータ数、呼び出し回数などのソフトウェアメトリクス、ソフトウェアの実行時エラーの特定といったメトリクスも生成します。[ 10 ]

参照

参考文献

  1. ^ Pele, Anne-Francoise (2007年4月25日). 「MathworksがPolySpace Technologiesを買収」 . EETimes. 2012年2月11日時点のオリジナルよりアーカイブ2010年8月13日閲覧。
  2. ^ MathWorks - Polyspace - 要件
  3. ^ Deutsch, Alain (2003-11-27). 「動的特性の静的検証」(PDF) . Polyspace Technologies. 2012年3月13日時点のオリジナル(PDF)からアーカイブ。 2014年5月17日閲覧
  4. ^ Pelé, Anne-Françoise (2007年4月25日). 「MathworksがPolySpace Technologiesを買収」 . EE Times . 2024年7月12日閲覧。
  5. ^ Brat, Guillaume (2004). 「火星探査車ソフトウェアにおける検証・妥当性確認ツールの実験的評価」.システム設計における形式手法. 25 (2/3): 167– 198. doi : 10.1023/B:FORM.0000040027.28662.a4 . hdl : 2060/20040010327 .
  6. ^ a b Exponent (2012年9月24日). 「ExponentによるトヨタETCS-i車両のハードウェアとソフトウェアの調査」 Exponent. 2014年7月27日時点のオリジナルよりアーカイブ2010年9月7日閲覧。
  7. ^ MathWorks:静的コード解析.
  8. ^ Jones, Paul; Jetley, Raoul; Abraham, Jay (2010-02-09). 「医療機器ソフトウェア解析における形式手法に基づく検証アプローチ」 . Embedded Systems Design . 2010年8月16日閲覧。
  9. ^ Wissing, Klaus (2007-09-27). 「動的プロパティの静的分析 - 動的実行時エラーの不在を証明するための自動プログラム検証」(PDF) . 応用プログラム分析ワークショップ. 2010-08-13閲覧.
  10. ^ 「ソフトウェアメトリクス-MATLAB」インド: MathWorks . 2015年8月27日閲覧