第一部分

Polyspace工作流程概覽

目標(biāo)：了解Polyspace Bug Finder與Code Prover并跑通一個例子程序

·?Polyspace與軟件開發(fā)流程

·?簡單驗證樣例

·?分析代碼中的缺陷與運行時錯誤

Polyspace Bug Finder分析

目標(biāo)：分析可能不符合ANSI C的代碼并配置運行時環(huán)境，使用 Bug Finder 糾正缺陷和編碼規(guī)則違規(guī)。

·?常見運行環(huán)境構(gòu)件

·?處理處理器特定代碼

·?定義執(zhí)行的上下文

·?設(shè)置目標(biāo)硬件信息

·?分析和管理Bug Finder發(fā)現(xiàn)的缺陷

·?檢測編碼規(guī)則沖突

·?度量代碼統(tǒng)計指標(biāo)

分析Polyspace Code Prover的結(jié)果

目標(biāo)：?能熟練解釋Polyspace Code Prover的結(jié)果。

·?抽象解釋概覽

·?調(diào)用層次分析

·?源代碼導(dǎo)航

·?執(zhí)行路徑

·?變量范圍

·?全局變量

代碼驗證中的檢查項

目標(biāo)：能熟練解讀Polyspace Code Prover的結(jié)果。

·?C代碼檢查項一覽

·?源代碼中的檢查項定位

·?檢查項描述

·?相關(guān)驗證選項

第二部分

管理Polyspace Code Prover驗證與結(jié)果

目標(biāo)：處理含有大量未證明檢查項的驗證結(jié)果。

·?判斷驗證開銷

·?進行快速評審

·?進行選擇性的橙色代碼評審

·?設(shè)置驗證精度

·?區(qū)分橙色檢查項優(yōu)先級

·?評審橙色檢查項

增加Polyspace Code Prover驗證精度

目標(biāo)：學(xué)習(xí)如何在用Polyspace Code Prover驗證代碼時處置缺失的代碼，以及如何對此施加影響從而產(chǎn)生更有意義的驗證結(jié)果。

·?魯棒性驗證與上下文驗證

·?函數(shù)打樁

·?數(shù)據(jù)范圍指定

·?手動打樁

集成分析

目標(biāo)：學(xué)習(xí)如何管理復(fù)雜性日益增加的代碼驗證，以及如何解釋并比較集成分析與健壯性分析。

·?管理代碼模塊

·?用Bug Finder與Code Prover分析集成缺陷與編碼違規(guī)

·?導(dǎo)入注釋

完整應(yīng)用分析

目標(biāo)：回顧對整個應(yīng)用進行完整驗證時的流程和選項。

·?創(chuàng)建應(yīng)用級驗證工程

·?改善應(yīng)用的驗證結(jié)果

·?發(fā)現(xiàn)并發(fā)訪問問題

·?對比健壯性驗證和上下文驗證

·?創(chuàng)建文檔

第三部分

實踐教學(xué)（選修）

目標(biāo)：花時間來回顧你學(xué)到的內(nèi)容并在你自己的項目上直接應(yīng)用 Polyspace. 潛在內(nèi)容包括：

·?Bug Finder 檢測

·?驗證 C++ 代碼

·?任務(wù)和共享數(shù)據(jù)分析

·?驗證生成的代碼

·?開發(fā)過程回顧

·?工作流程整合

·?客戶端/服務(wù)器軟件安裝

·?項目代碼的 Polyspace 配置

·?結(jié)果解釋