產品及服務 > Polyspace Code Prover™ , Polyspace程式碼驗證器
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)。

Key Features

  • 檢驗原始程式碼中特殊執行階段的錯誤。
  • 直接以顏色在程式碼中標明可能產生執行階段錯誤的程式碼。
  • 計算顯示變量的範圍資訊和函式回傳值
  • 針對超出規定邊界條件限制進行變數識別
  • 追踪品質條件完成狀態並確保符合軟體品質目標。
  • 以Web為基礎的顯示區來呈現程式碼的品質狀態
  • 具備引導重複確認流程,讓您在進行分類結果和確認執行階段錯誤時更容易。
  • 提供變量讀取及寫入的圖形顯示功能。
  • 支援 MISRA C:2012程式碼規則驗證
  • 2016a開始支援 long-double 浮點數資料型態,並且改進了對無窮大的值及非數值(NaN)的支援
  • 2016b支援 CERT C 編碼規範,以用於網路安全性漏洞檢測。