Polyspace Code Prover^™. Polyspace程式碼驗證器

Introduction

Polyspace程式碼驗證器(Polyspace Code Prover)，用於檢驗原始程式碼中溢位(absence of overflow)、除零、陣列越界(out-of-bounds array access)和驗證在C和C++程式碼中的其他執行階段錯誤(run-time errors)，且不需執行程式、進行程式碼探測或測試範例即可產生結果。Polyspace程式碼驗證器是以形式方法(formal methods)為基礎來進行靜態分析和抽象解譯。不論是手寫碼程式碼、由軟體產生的程式碼，或是在兩種混合的狀況下也可使用。每次執行檢測，系統均會以不同顏色標明程式碼，以表示它是否不會產生執行階段產生錯誤、驗證失敗，無法到達，或無法驗證等各種狀況。

Polyspace程式碼驗證器還可顯示範圍內的變量資訊以及函式回傳值，並在每一語句檢測其在執行過程中可能的邊界條件，並考慮程式碼中每一變數可能數值的範圍。之後將結果發布到顯示區(dashboard)，以追蹤品質條件完成狀態並確保符合軟體品質目標。 Polyspace程式碼驗證器可以整合到程式編譯系統來進行自動驗證。

Polyspace程式碼驗證器支援產業標準，包括IEC安全驗證套裝組( IEC Certification Kit (for IEC 61508 and ISO 26262)) 和DO品質驗證套裝組(DO Qualification Kit (for DO-178))，現在也支援Ada語言，及支援 MISRA C:2012程式碼規則驗證

本工具箱使用需搭配MATLAB、Polyspace程式碼查錯器(Polyspace Bug Finder)。