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

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

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

3、組成，成，支持支持u主流建模語(yǔ)言主流建模語(yǔ)言UMLUMLu主流主流軟件開(kāi)發(fā)語(yǔ)言軟件開(kāi)發(fā)語(yǔ)言C/C+/ C/C+/ JAVAJAVAu主要主要軟件缺陷的檢測(cè)：軟件缺陷的檢測(cè)： 內(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語(yǔ)言代碼分析和單元測(cè)試工具語(yǔ)言代碼分析和單元測(cè)試工具CAUTCAUTu面向?qū)ο蟪绦蚍治雠c測(cè)試工具面向?qū)ο蟪绦蚍治雠c測(cè)試工具QESatQESatu軟件測(cè)試過(guò)程管理工具軟件測(cè)試過(guò)程管理工具QESuiteQESuiteu軟件缺陷檢測(cè)工具軟件缺

4、陷檢測(cè)工具DTSDTSu線性混成系統(tǒng)可達(dá)性的有界模型檢驗(yàn)工具線性混成系統(tǒng)可達(dá)性的有界模型檢驗(yàn)工具BACHBACHu基于場(chǎng)景規(guī)約的時(shí)間性質(zhì)驗(yàn)證工具基于場(chǎng)景規(guī)約的時(shí)間性質(zhì)驗(yàn)證工具TASSTASSu基于基于UMLUML模型的測(cè)試和驗(yàn)證工具集模型的測(cè)試和驗(yàn)證工具集JasmineJasmine 基于活動(dòng)圖的測(cè)試用例生成工具基于活動(dòng)圖的測(cè)試用例生成工具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語(yǔ)言代碼分析和單元測(cè)試工具語(yǔ)言代碼分析和單元測(cè)試工具CAUTCAUTv基本功能基本功能 單元測(cè)試用例自動(dòng)生成單元測(cè)試用例自動(dòng)生成 代碼靜態(tài)代碼靜態(tài)檢查檢查v主要用途主要用途 針對(duì)針對(duì)C C程序，采用程序，采用靜態(tài)分析與動(dòng)態(tài)運(yùn)行相結(jié)合的方式，檢測(cè)靜態(tài)分析與動(dòng)態(tài)運(yùn)行相結(jié)合的方式，檢測(cè)由于內(nèi)存訪

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

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

8、于故障模式的缺陷檢測(cè)基于故障模式的缺陷檢測(cè) 基于安全漏洞模式的缺陷檢測(cè)基于安全漏洞模式的缺陷檢測(cè) 基于疑問(wèn)模式的缺陷檢測(cè)基于疑問(wèn)模式的缺陷檢測(cè) 基于規(guī)則模式的缺陷檢測(cè)基于規(guī)則模式的缺陷檢測(cè)v主要用途主要用途 針對(duì)針對(duì)C/C+/JavaC/C+/Java程序，利用靜態(tài)分析的程序，利用靜態(tài)分析的方法對(duì)源代碼中的軟件缺陷實(shí)施檢測(cè)。方法對(duì)源代碼中的軟件缺陷實(shí)施檢測(cè)。線性混成系統(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)?；趫?chǎng)景規(guī)約的時(shí)間性質(zhì)驗(yàn)證工具基于場(chǎng)景規(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ì)階段對(duì)場(chǎng)景規(guī)約的時(shí)間性質(zhì)做分析和驗(yàn)證。用于需求和設(shè)計(jì)階段對(duì)場(chǎng)景規(guī)約的時(shí)間性質(zhì)做分析和驗(yàn)證?？尚诺膰?guó)家軟件資源共享與協(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)圖的測(cè)試基于活動(dòng)圖的測(cè)試用例生成工具用例生成工具基于交互圖的動(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模型的測(cè)試和驗(yàn)證工具集模型的測(cè)試和驗(yàn)證工具集JasmineJ基于基于UMLUML模型的測(cè)試和驗(yàn)證工具集模型的測(cè)試和驗(yàn)證工具集JasmineJasminev基于活動(dòng)圖的測(cè)試用例生成工具基于活動(dòng)圖的測(cè)試用例生成工具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í)中的分類方法 有效地降低了測(cè)試用例生成的成本、提高了效率。有效地降低了測(cè)試用例生成的成本、提高了效率。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ī)約，針對(duì)動(dòng)態(tài)模型做為系統(tǒng)規(guī)約，針對(duì)JAVAJAVA程序進(jìn)行運(yùn)行時(shí)驗(yàn)證。程序進(jìn)行運(yùn)行時(shí)驗(yàn)證?？尚诺膰?guó)家軟件資源共享與協(xié)同生產(chǎn)環(huán)境

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

13、v評(píng)估與咨詢相結(jié)合評(píng)估與咨詢相結(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對(duì)相關(guān)技術(shù)與工具的能力模型和可擴(kuò)展空間的分析與評(píng)估課題其它方面工作進(jìn)展課題其它方面工作進(jìn)展專利、著作權(quán)專利、著作權(quán) 知識(shí)產(chǎn)權(quán)知識(shí)產(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國(guó)際期刊、國(guó)際會(huì)議和國(guó)內(nèi)一級(jí)國(guó)際期刊、國(guó)際會(huì)議和國(guó)內(nèi)一級(jí)學(xué)報(bào)學(xué)報(bào)4 40

14、0篇篇： 國(guó)際期刊國(guó)際期刊2 2篇篇Innovations in Systems and Software EngineeringInnovations in Systems and Software Engineering, , Springer Springer 國(guó)際學(xué)術(shù)會(huì)議國(guó)際學(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 國(guó)內(nèi)一級(jí)學(xué)報(bào)國(guó)內(nèi)一級(jí)學(xué)報(bào)1010篇篇 中國(guó)科學(xué)中國(guó)科學(xué)、軟件學(xué)報(bào)軟件學(xué)報(bào)、電子學(xué)報(bào)電子學(xué)報(bào)v專著專著3 3部、譯著部、譯著3 3部部課題其它方面工作進(jìn)展課題其它方面工作進(jìn)展知識(shí)產(chǎn)權(quán)知識(shí)產(chǎn)權(quán)v 獲得專利授權(quán)獲得專利授權(quán)1 1項(xiàng)項(xiàng) 基于倒排表進(jìn)行檢索提示的方

16、法基于倒排表進(jìn)行檢索提示的方法 v 申請(qǐng)技術(shù)專利申請(qǐng)技術(shù)專利1010項(xiàng)項(xiàng) 一種基于軟件缺陷模式的測(cè)試方法一種基于軟件缺陷模式的測(cè)試方法 應(yīng)用區(qū)間運(yùn)算的軟件測(cè)試方法應(yīng)用區(qū)間運(yùn)算的軟件測(cè)試方法 基于編輯距離的源代碼相似度度量方法基于編輯距離的源代碼相似度度量方法 用于多正則表達(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)試方法 軟件測(cè)試用例生成方法與系統(tǒng)軟件測(cè)試用例生成方法與系統(tǒng)v 獲得軟件著作權(quán)獲得軟件著作權(quán)1919項(xiàng)項(xiàng) Java Java軟件缺陷檢測(cè)系統(tǒng)軟件缺陷檢測(cè)系統(tǒng) C

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

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