第一部分

Polyspace工作流程概覽

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

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

·?簡(jiǎn)單驗(yàn)證樣例

·?分析代碼中的缺陷與運(yùn)行時(shí)錯(cuò)誤

Polyspace Bug Finder分析

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

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

·?處理處理器特定代碼

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

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

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

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

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

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

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

·?抽象解釋概覽

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

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

·?執(zhí)行路徑

·?變量范圍

·?全局變量

代碼驗(yàn)證中的檢查項(xiàng)

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

·?C代碼檢查項(xiàng)一覽

·?源代碼中的檢查項(xiàng)定位

·?檢查項(xiàng)描述

·?相關(guān)驗(yàn)證選項(xiàng)

第二部分

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

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

·?判斷驗(yàn)證開銷

·?進(jìn)行快速評(píng)審

·?進(jìn)行選擇性的橙色代碼評(píng)審

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

·?區(qū)分橙色檢查項(xiàng)優(yōu)先級(jí)

·?評(píng)審橙色檢查項(xiàng)

增加Polyspace Code Prover驗(yàn)證精度

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

·?魯棒性驗(yàn)證與上下文驗(yàn)證

·?函數(shù)打樁

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

·?手動(dòng)打樁

集成分析

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

·?管理代碼模塊

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

·?導(dǎo)入注釋

完整應(yīng)用分析

目標(biāo)：回顧對(duì)整個(gè)應(yīng)用進(jìn)行完整驗(yàn)證時(shí)的流程和選項(xiàng)。

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

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

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

·?對(duì)比健壯性驗(yàn)證和上下文驗(yàn)證

·?創(chuàng)建文檔

第三部分

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

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

·?Bug Finder 檢測(cè)

·?驗(yàn)證 C++ 代碼

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

·?驗(yàn)證生成的代碼

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

·?工作流程整合

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

·?項(xiàng)目代碼的 Polyspace 配置

·?結(jié)果解釋