Polyspace
| 開発元 | MathWorks [1] |
|---|---|
| 最新版 |
R2019a
/ 2019年3月15日 |
| 対応OS | クロスプラットフォーム[2] |
| 種別 | 静的コード解析 |
| ライセンス | Proprietary |
| 公式サイト |
www |
Polyspaceは、静的コード解析ツール。C言語、C++、Adaのソースコードに実行時エラーが存在しないことを検出または証明するための抽象解釈による大規模分析ができる。このツールはソースコードが適切なコード標準に準拠しているかどうかもチェックできる。[3]
一般的な利用法
[編集]Polyspaceはソースコードを調べて算術オーバーフロー、バッファオーバーラン、ゼロ除算などの潜在的なランタイムエラーが発生する可能性のある場所を特定する。ソフトウェア開発者と品質保証マネージャーは、この情報を使用して、コードのどの部分に欠陥があるか、または信頼できることが証明されているかを特定する。コードの他の部分は、証明されていないチェック用にマークされており、個別にレビューするべきである。[4][5]
MISRA Cなどのコード標準またはコーディング規約はコードの品質、移植性、および信頼性に取り組もうとする。この製品はC言語およびC++のソースコードがこれらのコード標準のルールの一部に適合しているかどうかをチェックする。[6]
Capabilities
[編集]![[icon]](/wiki/%E3%83%95%E3%82%A1%E3%82%A4%E3%83%AB:OOjs_UI_icon_language-ltr-progressive.svg){kind=icon} |
The product family consists of Polyspace Code Prover and Polyspace Bug Finder. The Code Prover module annotates source code with a color-coding scheme to indicate the status of each element in the code.[7] It uses formal methods-based static code analysis to verify program execution at the language level.[5] The tool checks each code instruction by taking into account all possible values of every variable at every point in the code, providing a formal diagnostic for each operation in the code under both normal and abnormal usage conditions.[8]
The Bug Finder module identifies software bugs by performing static program analysis on source code. It finds defects such as numerical computation, programming, memory, and other errors. It also produces software metrics such as Comment density of a source file, Cyclomatic complexity, Number of lines, parameters, call levels, etc. in a function, Identified run-time errors in the software.[9]
脚注
[編集]- ^ Pele, Anne-Francoise (2007年4月25日). “The Mathworks acquires PolySpace Technologies”. EETimes. 2012年2月11日時点のオリジナルよりアーカイブ。2010年8月13日閲覧。
- ^ The MathWorks - Polyspace - Requirements
- ^ Deutsch, Alain (2003年11月27日). “Static Verification of Dynamic Properties”. Polyspace Technologies. 2012年3月13日時点のオリジナルよりアーカイブ。2014年5月17日閲覧。
- ^ Brat, Guillaume (2004). “Experimental Evaluation of Verification and Validation Tools on Martian Rover Software”. Formal Methods in System Design 25 (2/3): 167–198. doi:10.1023/B:FORM.0000040027.28662.a4. hdl:2060/20040010327.
- ^ a b Exponent (2012年9月24日). “Exponent's Investigation of Toyota ETCS-i Vehicle Hardware and Software”. Exponent. 2014年7月27日時点のオリジナルよりアーカイブ。2010年9月7日閲覧。
- ^ MathWorks. “static code analysis”. 2020年10月21日閲覧。
- ^ “A Formal Methods-based verification approach to medical device software analysis”. Embedded Systems Design (2010年2月9日). 2010年8月16日閲覧。
- ^ Wissing, Klaus (2007年9月27日). “Static Analysis of Dynamic Properties - Automatic Program Verification to Prove the Absence of Dynamic Runtime Errors”. Workshop on Applied Program Analysis. 2010年8月13日閲覧。
- ^ “Software Metrics-MATLAB”. India: MathWorks. 2015年8月27日閲覧。
関連項目
[編集]外部リンク
[編集]- Polyspace - MATLAB & Simulink 公式ウェブサイト