支持軟件可信性分析和評估的生產(chǎn)線

1、可信 共享 協(xié)同支持軟件可信性分析和評估的生產(chǎn)線支持軟件可信性分析和評估的生產(chǎn)線南京大學(xué)南京大學(xué) 北京航空航天大學(xué)北京航空航天大學(xué)華東師范大學(xué)華東師范大學(xué) 北京郵電大學(xué)北京郵電大學(xué)2009.6.1 2009.6.1 北京北京匯報(bào)提綱匯報(bào)提綱生產(chǎn)線解決的問題生產(chǎn)線解決的問題1生產(chǎn)線的組成生產(chǎn)線的組成2生產(chǎn)線各類工具簡介生產(chǎn)線各類工具簡介3課題其它方面進(jìn)展課題其它方面進(jìn)展5下一步工作重點(diǎn)下一步工作重點(diǎn)6可信性評估與咨詢體系階段性工作可信性評估與咨詢體系階段性工作生產(chǎn)線解決的問題生產(chǎn)線解決的問題p針對可信軟件的關(guān)鍵技術(shù)需求，面向軟件生針對可信軟件的關(guān)鍵技術(shù)需求，面向軟件生命周期各個(gè)階段的制品，通過軟

2、件分析、測命周期各個(gè)階段的制品，通過軟件分析、測試和驗(yàn)證途徑認(rèn)識與理解軟件系統(tǒng)，提高軟試和驗(yàn)證途徑認(rèn)識與理解軟件系統(tǒng)，提高軟件系統(tǒng)的可信性，為建立人與軟件系統(tǒng)之間件系統(tǒng)的可信性，為建立人與軟件系統(tǒng)之間的信任關(guān)系提供依據(jù)。的信任關(guān)系提供依據(jù)。p提高軟件分析、測試和驗(yàn)證技提高軟件分析、測試和驗(yàn)證技術(shù)的有效性、可擴(kuò)展性、自動(dòng)術(shù)的有效性、可擴(kuò)展性、自動(dòng)化程度，降低可信軟件成本?；潭龋档涂尚跑浖杀?。生產(chǎn)線組成生產(chǎn)線組成 p生產(chǎn)線面向軟件生命周期，由針對軟件規(guī)約、模型、生產(chǎn)線面向軟件生命周期，由針對軟件規(guī)約、模型、代碼和缺陷的一組分析、測試、驗(yàn)證和評估工具組代碼和缺陷的一組分析、測試、驗(yàn)證和評估工具

3、組成，成，支持支持u主流建模語言主流建模語言UMLUMLu主流主流軟件開發(fā)語言軟件開發(fā)語言C/C+/ C/C+/ JAVAJAVAu主要主要軟件缺陷的檢測：軟件缺陷的檢測： 內(nèi)存泄露內(nèi)存泄露 緩沖區(qū)溢出緩沖區(qū)溢出 死鎖死鎖/ /指針誤用指針誤用/ /風(fēng)格缺陷等風(fēng)格缺陷等生產(chǎn)線組成生產(chǎn)線組成 生產(chǎn)線組成生產(chǎn)線組成 p生產(chǎn)線包括以下工具：生產(chǎn)線包括以下工具：uC C語言代碼分析和單元測試工具語言代碼分析和單元測試工具CAUTCAUTu面向?qū)ο蟪绦蚍治雠c測試工具面向?qū)ο蟪绦蚍治雠c測試工具QESatQESatu軟件測試過程管理工具軟件測試過程管理工具QESuiteQESuiteu軟件缺陷檢測工具軟件缺

4、陷檢測工具DTSDTSu線性混成系統(tǒng)可達(dá)性的有界模型檢驗(yàn)工具線性混成系統(tǒng)可達(dá)性的有界模型檢驗(yàn)工具BACHBACHu基于場景規(guī)約的時(shí)間性質(zhì)驗(yàn)證工具基于場景規(guī)約的時(shí)間性質(zhì)驗(yàn)證工具TASSTASSu基于基于UMLUML模型的測試和驗(yàn)證工具集模型的測試和驗(yàn)證工具集JasmineJasmine 基于活動(dòng)圖的測試用例生成工具基于活動(dòng)圖的測試用例生成工具Jasmine-ADGJasmine-ADG 基于活動(dòng)圖的動(dòng)態(tài)驗(yàn)證工具基于活動(dòng)圖的動(dòng)態(tài)驗(yàn)證工具Jasmine-ADVJasmine-ADV 基于交互圖的動(dòng)態(tài)驗(yàn)證工具基于交互圖的動(dòng)態(tài)驗(yàn)證工具Jasmine-IODVJasmine-IODV 基于狀態(tài)圖的動(dòng)態(tài)驗(yàn)證

5、工具基于狀態(tài)圖的動(dòng)態(tài)驗(yàn)證工具Jasmine-SCVJasmine-SCV 基于順序圖的動(dòng)態(tài)驗(yàn)證工具基于順序圖的動(dòng)態(tài)驗(yàn)證工具Jasmine-SDVJasmine-SDVp工具的研發(fā)宗旨：工具的研發(fā)宗旨：u比別人能力強(qiáng)比別人能力強(qiáng)u比別人抓得準(zhǔn)比別人抓得準(zhǔn)u比別人跑得快比別人跑得快u比別人價(jià)格低比別人價(jià)格低C C語言代碼分析和單元測試工具語言代碼分析和單元測試工具CAUTCAUTv基本功能基本功能 單元測試用例自動(dòng)生成單元測試用例自動(dòng)生成 代碼靜態(tài)代碼靜態(tài)檢查檢查v主要用途主要用途 針對針對C C程序，采用程序，采用靜態(tài)分析與動(dòng)態(tài)運(yùn)行相結(jié)合的方式，檢測靜態(tài)分析與動(dòng)態(tài)運(yùn)行相結(jié)合的方式，檢測由于內(nèi)存訪

6、問違例而導(dǎo)致的程序由于內(nèi)存訪問違例而導(dǎo)致的程序崩潰、斷言崩潰、斷言違反等常見違反等常見的的運(yùn)行時(shí)錯(cuò)誤。運(yùn)行時(shí)錯(cuò)誤。面向?qū)ο蟪绦蚍治雠c測試工具面向?qū)ο蟪绦蚍治雠c測試工具QESatQESatv基本功能基本功能 自動(dòng)代碼缺陷檢測自動(dòng)代碼缺陷檢測 人工輔助代碼審查人工輔助代碼審查 軟件結(jié)構(gòu)審查軟件結(jié)構(gòu)審查 軟件動(dòng)態(tài)覆蓋率分析軟件動(dòng)態(tài)覆蓋率分析v主要用途主要用途 提供對提供對JavaJava和和C+C+兩種語言的支持，能幫兩種語言的支持，能幫助分析助分析JavaJava和和C C+程程序，使程序員更快捷有效地理解程序結(jié)構(gòu)，及早地發(fā)現(xiàn)程序序，使程序員更快捷有效地理解程序結(jié)構(gòu)，及早地發(fā)現(xiàn)程序中隱藏的錯(cuò)誤，提

7、高程序的質(zhì)量中隱藏的錯(cuò)誤，提高程序的質(zhì)量軟件測試過程管理工具軟件測試過程管理工具QESuiteQESuitev基本功能基本功能 測試需求管理測試需求管理 測試計(jì)劃管理測試計(jì)劃管理 測試過程的定義與監(jiān)控測試過程的定義與監(jiān)控 測試用例追蹤和管理測試用例追蹤和管理 軟件問題報(bào)告（軟件缺陷）軟件問題報(bào)告（軟件缺陷）的全的全生命生命期追蹤和管理期追蹤和管理 基于測試數(shù)據(jù)的被測基于測試數(shù)據(jù)的被測軟件可信性軟件可信性度量度量和評估和評估v主要主要用途用途 支持對軟件全生命周期、符合可信軟支持對軟件全生命周期、符合可信軟件測試要求的軟件測試過程進(jìn)行管理。件測試要求的軟件測試過程進(jìn)行管理。v基本功能基本功能 基

8、于故障模式的缺陷檢測基于故障模式的缺陷檢測 基于安全漏洞模式的缺陷檢測基于安全漏洞模式的缺陷檢測 基于疑問模式的缺陷檢測基于疑問模式的缺陷檢測 基于規(guī)則模式的缺陷檢測基于規(guī)則模式的缺陷檢測v主要用途主要用途 針對針對C/C+/JavaC/C+/Java程序，利用靜態(tài)分析的程序，利用靜態(tài)分析的方法對源代碼中的軟件缺陷實(shí)施檢測。方法對源代碼中的軟件缺陷實(shí)施檢測。線性混成系統(tǒng)可達(dá)性的有界模型檢驗(yàn)工具線性混成系統(tǒng)可達(dá)性的有界模型檢驗(yàn)工具BACHBACHv基本功能基本功能 線性混成自動(dòng)機(jī)可視化編輯線性混成自動(dòng)機(jī)可視化編輯 面向單路徑的可達(dá)性驗(yàn)證面向單路徑的可達(dá)性驗(yàn)證 有界全路徑的可達(dá)性驗(yàn)證有界全路徑的可

9、達(dá)性驗(yàn)證v主要用途主要用途 支持線性混成系統(tǒng)的可達(dá)性驗(yàn)證，能夠?qū)χС志€性混成系統(tǒng)的可達(dá)性驗(yàn)證，能夠?qū)Υ笠?guī)模系統(tǒng)的關(guān)鍵路徑進(jìn)行深層次的檢驗(yàn)。大規(guī)模系統(tǒng)的關(guān)鍵路徑進(jìn)行深層次的檢驗(yàn)?；趫鼍耙?guī)約的時(shí)間性質(zhì)驗(yàn)證工具基于場景規(guī)約的時(shí)間性質(zhì)驗(yàn)證工具TASSTASSv基本功能基本功能 可達(dá)性驗(yàn)證可達(dá)性驗(yàn)證 時(shí)間約束滿足性驗(yàn)證時(shí)間約束滿足性驗(yàn)證 事件間隔延時(shí)驗(yàn)證事件間隔延時(shí)驗(yàn)證v主要用途主要用途 用于需求和設(shè)計(jì)階段對場景規(guī)約的時(shí)間性質(zhì)做分析和驗(yàn)證。用于需求和設(shè)計(jì)階段對場景規(guī)約的時(shí)間性質(zhì)做分析和驗(yàn)證?？尚诺膰臆浖Y源共享與協(xié)同生產(chǎn)環(huán)境 第二次總體技術(shù)會(huì)議 基于活動(dòng)圖的動(dòng)基于活動(dòng)圖的動(dòng)態(tài)驗(yàn)證工具態(tài)驗(yàn)證工具基于活

10、動(dòng)圖的測試基于活動(dòng)圖的測試用例生成工具用例生成工具基于交互圖的動(dòng)基于交互圖的動(dòng)態(tài)驗(yàn)證工具態(tài)驗(yàn)證工具基于狀態(tài)圖的動(dòng)基于狀態(tài)圖的動(dòng)態(tài)驗(yàn)證工具態(tài)驗(yàn)證工具基于順序圖的動(dòng)基于順序圖的動(dòng)態(tài)驗(yàn)證工具態(tài)驗(yàn)證工具基于基于UMLUML模型的測試和驗(yàn)證工具集模型的測試和驗(yàn)證工具集JasmineJ基于基于UMLUML模型的測試和驗(yàn)證工具集模型的測試和驗(yàn)證工具集JasmineJasminev基于活動(dòng)圖的測試用例生成工具基于活動(dòng)圖的測試用例生成工具Jasmine-ADGJasmine-ADG UMLUML活動(dòng)圖模型作為系統(tǒng)規(guī)約活動(dòng)圖模型作為系統(tǒng)規(guī)約 以模型路徑覆蓋為依據(jù)以模型路徑覆蓋為依據(jù) 在隨機(jī)方法的基礎(chǔ)上引入動(dòng)態(tài)反饋

11、機(jī)制在隨機(jī)方法的基礎(chǔ)上引入動(dòng)態(tài)反饋機(jī)制 結(jié)合機(jī)器學(xué)習(xí)中的分類方法結(jié)合機(jī)器學(xué)習(xí)中的分類方法 有效地降低了測試用例生成的成本、提高了效率。有效地降低了測試用例生成的成本、提高了效率。v基于基于UMLUML動(dòng)態(tài)模型的運(yùn)行時(shí)驗(yàn)證工具動(dòng)態(tài)模型的運(yùn)行時(shí)驗(yàn)證工具 Jasmine-ADVJasmine-ADV Jasmine-IODVJasmine-IODV Jasmine-SCVJasmine-SCV Jasmine-SDVJasmine-SDVn以以UMLUML動(dòng)態(tài)模型做為系統(tǒng)規(guī)約，針對動(dòng)態(tài)模型做為系統(tǒng)規(guī)約，針對JAVAJAVA程序進(jìn)行運(yùn)行時(shí)驗(yàn)證。程序進(jìn)行運(yùn)行時(shí)驗(yàn)證?？尚诺膰臆浖Y源共享與協(xié)同生產(chǎn)環(huán)境

12、第二次總體技術(shù)會(huì)議 軟件可信性評估和咨詢體系階段性工作軟件可信性評估和咨詢體系階段性工作v基于認(rèn)識與理解途徑的可信性分析與評估基于認(rèn)識與理解途徑的可信性分析與評估 目的：建立人與軟件之間的信任關(guān)系目的：建立人與軟件之間的信任關(guān)系 分析和評估軟件系統(tǒng)分析和評估軟件系統(tǒng) 滿足需求的程度滿足需求的程度 擺脫缺陷的程度擺脫缺陷的程度 途徑：軟件分析、測試、驗(yàn)證途徑：軟件分析、測試、驗(yàn)證 維度：模型、代碼、缺陷維度：模型、代碼、缺陷不同的軟件需求不同不同的軟件需求不同不同的軟件的缺陷不同的軟件的缺陷經(jīng)常相同經(jīng)常相同針對缺陷的評估與咨詢v死鎖等并發(fā)缺陷死鎖等并發(fā)缺陷v內(nèi)存泄露內(nèi)存泄露v緩沖區(qū)溢出緩沖區(qū)溢出

13、v評估與咨詢相結(jié)合評估與咨詢相結(jié)合內(nèi)存泄露（分析途徑）靜態(tài)分析動(dòng)態(tài)分析類型 1類型 2類型 n類型 1類型 2類型 n度量指標(biāo)度量指標(biāo)度量指標(biāo)度量指標(biāo)度量指標(biāo)度量指標(biāo)FastcheckMatalPREfixLCPurifyInsure+ccallocmpatrol對相關(guān)技術(shù)與工具的能力模型和可擴(kuò)展空間的分析與評估課題其它方面工作進(jìn)展課題其它方面工作進(jìn)展專利、著作權(quán)專利、著作權(quán) 知識產(chǎn)權(quán)知識產(chǎn)權(quán)技術(shù)創(chuàng)新技術(shù)創(chuàng)新 論文、論著論文、論著成果轉(zhuǎn)化成果轉(zhuǎn)化 示范應(yīng)用示范應(yīng)用課題其它方面工作進(jìn)展課題其它方面工作進(jìn)展技術(shù)創(chuàng)新技術(shù)創(chuàng)新v國際期刊、國際會(huì)議和國內(nèi)一級國際期刊、國際會(huì)議和國內(nèi)一級學(xué)報(bào)學(xué)報(bào)4 40

14、0篇篇： 國際期刊國際期刊2 2篇篇Innovations in Systems and Software EngineeringInnovations in Systems and Software Engineering, , Springer Springer 國際學(xué)術(shù)會(huì)議國際學(xué)術(shù)會(huì)議2828篇篇 CAV2009CAV2009、FMCAD2008FMCAD2008 ICST2008ICST2008、SAC2008SAC2008、IWMSE2008IWMSE2008、TASE2008 TASE2008 、 ICECCS2008ICECCS2008、FORTE2008FORTE2008、IC

15、TAC2008ICTAC2008、 SCAM2008SCAM2008、APSEC2008APSEC2008、TTSS2008TTSS2008、FACS2008FACS2008、HASE2008HASE2008、ICDCI2008ICDCI2008、UTP2008UTP2008、ISOLA2008ISOLA2008、SAC2009SAC2009 國內(nèi)一級學(xué)報(bào)國內(nèi)一級學(xué)報(bào)1010篇篇 中國科學(xué)中國科學(xué)、軟件學(xué)報(bào)軟件學(xué)報(bào)、電子學(xué)報(bào)電子學(xué)報(bào)v專著專著3 3部、譯著部、譯著3 3部部課題其它方面工作進(jìn)展課題其它方面工作進(jìn)展知識產(chǎn)權(quán)知識產(chǎn)權(quán)v 獲得專利授權(quán)獲得專利授權(quán)1 1項(xiàng)項(xiàng) 基于倒排表進(jìn)行檢索提示的方

16、法基于倒排表進(jìn)行檢索提示的方法 v 申請技術(shù)專利申請技術(shù)專利1010項(xiàng)項(xiàng) 一種基于軟件缺陷模式的測試方法一種基于軟件缺陷模式的測試方法 應(yīng)用區(qū)間運(yùn)算的軟件測試方法應(yīng)用區(qū)間運(yùn)算的軟件測試方法 基于編輯距離的源代碼相似度度量方法基于編輯距離的源代碼相似度度量方法 用于多正則表達(dá)式聯(lián)合搜索的擴(kuò)展有限狀態(tài)機(jī)及搜索方法用于多正則表達(dá)式聯(lián)合搜索的擴(kuò)展有限狀態(tài)機(jī)及搜索方法 LR LR（K K）文法任意文法位置的斷點(diǎn)調(diào)試方法）文法任意文法位置的斷點(diǎn)調(diào)試方法 軟件測試用例生成方法與系統(tǒng)軟件測試用例生成方法與系統(tǒng)v 獲得軟件著作權(quán)獲得軟件著作權(quán)1919項(xiàng)項(xiàng) Java Java軟件缺陷檢測系統(tǒng)軟件缺陷檢測系統(tǒng) C

17、C程序缺陷缺陷檢測系統(tǒng)程序缺陷缺陷檢測系統(tǒng) C C程序缺陷缺陷檢測系統(tǒng)程序缺陷缺陷檢測系統(tǒng) 課題其它方面工作進(jìn)展課題其它方面工作進(jìn)展成果轉(zhuǎn)化成果轉(zhuǎn)化v軟件缺陷自動(dòng)檢測工具已初步應(yīng)用于軟件缺陷自動(dòng)檢測工具已初步應(yīng)用于“神舟神舟-7-7”系統(tǒng)的測試系統(tǒng)的測試 對對“神舟神舟-7-7”系統(tǒng)中系統(tǒng)中8 8個(gè)軟件實(shí)施了測試，發(fā)個(gè)軟件實(shí)施了測試，發(fā)現(xiàn)了其中的現(xiàn)了其中的1313個(gè)故障個(gè)故障 。 與總裝備部軟件評測中心簽署了合作協(xié)議，與總裝備部軟件評測中心簽署了合作協(xié)議，擬在擬在“神舟工程神舟工程”、“探月工程探月工程” 系統(tǒng)中系統(tǒng)中進(jìn)一步的合作。進(jìn)一步的合作。v部分工具已經(jīng)在實(shí)際的軟件測試中使用部分工具已經(jīng)

18、在實(shí)際的軟件測試中使用 奧運(yùn)會(huì)信息發(fā)布系統(tǒng)的測試奧運(yùn)會(huì)信息發(fā)布系統(tǒng)的測試 7 7個(gè)子系統(tǒng)個(gè)子系統(tǒng) 5 5輪測試的問題數(shù)：輪測試的問題數(shù)： 108=31+34+20+23+0108=31+34+20+23+0 4 4個(gè)國防軟件系統(tǒng)的測試、個(gè)國防軟件系統(tǒng)的測試、 1 1個(gè)政府辦公系統(tǒng)的測試個(gè)政府辦公系統(tǒng)的測試課題其它方面工作進(jìn)展課題其它方面工作進(jìn)展成果轉(zhuǎn)化成果轉(zhuǎn)化v部分工具已在多個(gè)單位試用部分工具已在多個(gè)單位試用 國家火炬高技術(shù)產(chǎn)業(yè)開發(fā)中心國家火炬高技術(shù)產(chǎn)業(yè)開發(fā)中心 全國全國3535個(gè)軟件園或基地個(gè)軟件園或基地 南方電網(wǎng)、北方電網(wǎng)、珠海軟件評測中心南方電網(wǎng)、北方電網(wǎng)、珠海軟件評測中心 全軍全軍軟件評測中心軟件評測中心 總參二部軟件評測總參二部軟件評測中心中心 總裝軟件評測中心總裝軟件評測中心 總參機(jī)要局軟件評測中心總參機(jī)要