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

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

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

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)可達性的有界模型檢驗工具線性混成系統(tǒng)可達性的有界模型檢驗工具BACHBACHu基于場景規(guī)約的時間性質(zhì)驗證工具基于場景規(guī)約的時間性質(zhì)驗證工具TASSTASSu基于基于UMLUML模型的測試和驗證工具集模型的測試和驗證工具集JasmineJasmine 基于活動圖的測試用例生成工具基于活動圖的測試用例生成工具Jasmine-ADGJasmine-ADG 基于活動圖的動態(tài)驗證工具基于活動圖的動態(tài)驗證工具Jasmine-ADVJasmine-ADV 基于交互圖的動態(tài)驗證工具基于交互圖的動態(tài)驗證工具Jasmine-IODVJasmine-IODV 基于狀態(tài)圖的動態(tài)驗證

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

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

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

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

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

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

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

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

13、v評估與咨詢相結(jié)合評估與咨詢相結(jié)合內(nèi)存泄露（分析途徑）靜態(tài)分析動態(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ù)與工具的能力模型和可擴展空間的分析與評估課題其它方面工作進展課題其它方面工作進展專利、著作權(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)用課題其它方面工作進展課題其它方面工作進展技術(shù)創(chuàng)新技術(shù)創(chuàng)新v國際期刊、國際會議和國內(nèi)一級國際期刊、國際會議和國內(nèi)一級學(xué)報學(xué)報4 40

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

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

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

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