軟件學(xué)報安全攸關(guān)軟件系統(tǒng)建模與驗證專題

軟件學(xué)報安全攸關(guān)軟件系統(tǒng)建模與驗證專題文章整體分類1《基于形式化方法的航空電子系統(tǒng)檢測》方法：模型檢測質(zhì)量：一致性——系統(tǒng)結(jié)構(gòu)設(shè)計的資源是否滿足需求中性能指標(biāo)的配置要求，即：系統(tǒng)結(jié)構(gòu)對應(yīng)的資源能否滿足配置（靜態(tài)檢測）；可用性——系統(tǒng)的執(zhí)行環(huán)境是否能保證系統(tǒng)任務(wù)的正常執(zhí)行（動態(tài)檢測）。模型：系統(tǒng)結(jié)構(gòu)、資源、任務(wù)的形式化建模檢測標(biāo)準(zhǔn)：一致性——a.配置文件一致性：軟件配置項是否滿足需求（不同級別配置文件是否一致）；b.系統(tǒng)環(huán)境狀態(tài)適配性（環(huán)境即資源，當(dāng)前狀態(tài)能否滿足性能指標(biāo)）?？捎眯浴傻摹皺z測用例”。實例：航空電子系統(tǒng)仿真平臺《基于形式化方法的航空電子系統(tǒng)檢測》航空電子系統(tǒng)靜態(tài)建模API：輸入/輸出+約束；性能指標(biāo)PI：資源屬性名+數(shù)量；配置文件CONF：文件屬性+屬性值；軟件配置項CSCI：1+2+3；分系統(tǒng)SS：1+2+3+4；航空電子系統(tǒng)ES：1+2+3+5.功能建模組件關(guān)系建?！痘谛问交椒ǖ暮娇针娮酉到y(tǒng)檢測》動態(tài)建模：窗口樹、任務(wù)執(zhí)行過程狀態(tài)圖《基于形式化方法的航空電子系統(tǒng)檢測》檢測過程2《基于時間抽象狀態(tài)機的AADL模型驗證》方法：模型檢測實際工作：AADL（系統(tǒng)體系結(jié)構(gòu)設(shè)計與分析語言）

TASM（時間抽象狀態(tài)機）質(zhì)量：依賴于TASMToolset和UPPAAL模型：AADL圖形化模型檢測標(biāo)準(zhǔn)：任務(wù)的參數(shù)描述（表格）實例：導(dǎo)航、制導(dǎo)與控制系統(tǒng)GNC的AOCS子系統(tǒng)（控制計算機/姿勢與軌道控制系統(tǒng)）工具：AADL2TASM《基于時間抽象狀態(tài)機的AADL模型驗證》思路：1.分別對AADL和TASM語法進行抽象，然后給出映射關(guān)系，并基于ML的元語言形式定義2者的轉(zhuǎn)換語義規(guī)則；2.系統(tǒng)AADL建模AADL2TASMTASMToolSet分析完整性、一致性、時間行為和資源行為仿真UPPAAL檢測死鎖、安全性、活性、實時性。3《基于時間STM的軟件形式化建模與驗證方法》方法：模型檢測質(zhì)量：可信性（時間和邏輯屬性）模型：TSTM——給STM加了‘時間和語義約束’（STM——狀態(tài)遷移矩陣，一種基于表結(jié)構(gòu)的狀態(tài)機建模方法，前端為表格形式，后端是嚴(yán)格的形式化定義）檢測標(biāo)準(zhǔn)：用‘時序邏輯語言’TCLT定義的所需滿足的性質(zhì)。實例：列車控制系統(tǒng)3《基于時間STM的軟件形式化建模與驗證方法》本文方法：軟件TSTM建模，刻畫軟件的行為特征；屬性的TCTL描述檢測方法：基于界限模型檢測（BMC）技術(shù)的‘時間計算樹邏輯（TCTL）’模型檢測方法——模型和待驗證屬性的否定形式進行合取，構(gòu)建BMC公式，BMC公式的求解問題歸約為邏輯公式的可滿足性判定，即：SAT/SMT實例。4《設(shè)備驅(qū)動程序可靠性和正確性保障方法與技術(shù)研究進展》綜述性論文質(zhì)量：驅(qū)動程序的可靠性和正確性。程序故障隔離與恢復(fù)、正確性分析和驗證、設(shè)計建模與復(fù)雜性控制。5《基于數(shù)據(jù)鏈的軟件故障定位方法》方法：代碼分析質(zhì)量：程序的數(shù)據(jù)流相關(guān)的邏輯故障定位（程序設(shè)計邏輯故障，定位到方法內(nèi)的代碼）模型：數(shù)據(jù)鏈——每個變量上的‘定義操作狀態(tài)軌跡’及其之間的依賴關(guān)系。分析對象：程序代碼檢測方法：先用現(xiàn)有方法將邏輯故障定位到方法；再用本文方法中方法內(nèi)定為——變量故障疑似度分析：a.對故障疑似方法建立‘?dāng)?shù)據(jù)鏈’；b.用a的數(shù)據(jù)鏈構(gòu)建概率數(shù)據(jù)鏈模型。c.疑似度排序?qū)嶒瀸Ρ?《一種面向列車控制系統(tǒng)中安全攸關(guān)場景的測試用例自動生成方法》本文工作：擴展了活動圖，加入了a.事件驅(qū)動機制；b.時間約束.覆蓋準(zhǔn)則：a.循環(huán)只執(zhí)行一次；b.不同的并發(fā)分支并發(fā)執(zhí)行（同時向前執(zhí)行一步）；c.所有‘簡單路徑’被覆蓋（從a、b兩條準(zhǔn)則得到的活動圖執(zhí)行路徑）。本文測試用例生成方法：擴展活動圖建模，并找出其中的‘簡單路徑’；明確‘被測系統(tǒng)’的邊界；執(zhí)行簡單路徑，并沿路收集外部環(huán)境向被測系統(tǒng)發(fā)送的事件，作為‘測試輸入’，被測系統(tǒng)向外部環(huán)境的輸出作為‘結(jié)果序列’。測試用例=環(huán)境傳給被測系統(tǒng)的信息（特定時間）+被測系統(tǒng)的觀察結(jié)果+時間上需滿足的約束。實例：地鐵列車控制系統(tǒng)7《多處理器實時系統(tǒng)可調(diào)度分析的UPPAAL模型》方法:模型檢測（偏硬件，主要數(shù)UPPAAL的使用）質(zhì)量：可調(diào)度性——系統(tǒng)必須滿足的時間要求。模型：UPPAAL模型性質(zhì)：時間自動機建模可調(diào)度性相關(guān)的模塊（實時任務(wù)、運行平臺、調(diào)度管理）檢測：UPPAAL檢測實驗：對象——智能手機GSM系統(tǒng)的21個任務(wù)本文貢獻：給出了多處理器實時系統(tǒng)可調(diào)度分析的模板8《多分支單變量循環(huán)程序的終止性分析》方法：代碼分析質(zhì)量：帶多個分支的單變量循環(huán)程序的終止性問題（系統(tǒng)中有無死循環(huán)，是正確性的基礎(chǔ)）（可信計算）主要結(jié)果：稱由迭代函數(shù)F和循環(huán)條件形成的區(qū)域I所構(gòu)成的循環(huán)程序P(F,I)在實數(shù)域\是不可終止的,如果存在一點x0∈\,使得{()}FxIi00i+∞=?.這里,Fi=FDFD…DF表示函數(shù)的復(fù)合.如果那樣的x0不存在,則稱循環(huán)P(F,I)在實數(shù)域上可終止.定理1.令f:R6R為一維連續(xù)映射.I為一閉區(qū)間.循環(huán)程序

P1Whilex∈Ido

{x:=f(x)}

是不可終止的充分必要條件為迭代映射f在閉區(qū)間I上有不動點.……實例應(yīng)用：對多分支單變量多項式循環(huán)程序，可通過實代數(shù)工具驗證定理中條件是否成立；判定不動點是否落入到循環(huán)條件形成的區(qū)域問題，可轉(zhuǎn)為半代數(shù)系統(tǒng)，通過實代數(shù)工具求解。

9《面向安全攸關(guān)系統(tǒng)中小概率事件的統(tǒng)計模型檢測》方法：基于機器學(xué)習(xí)的統(tǒng)計模型檢測算法統(tǒng)計模型檢測SMC——評估系統(tǒng)模型滿足屬性約束的概率區(qū)間機器學(xué)習(xí)（用于生成更多樣本）質(zhì)量：可靠性（在相對較少的樣本數(shù)量下，預(yù)測、評估小概率事件的發(fā)生概率）本文框架：輸入：a.目標(biāo)系統(tǒng)的可執(zhí)行模型（隨機混成自動機模型SHA）；b.屬性約束的‘概率有界線性時態(tài)邏輯（PBLTL公式）’；c.統(tǒng)計精度參數(shù)。輸出：在有限的資源約束下，系統(tǒng)模型a滿足屬性約束b的概率區(qū)間。2個模塊：學(xué)習(xí)型模型檢測器+自適應(yīng)統(tǒng)計分析器實例：基于通信的列車控制系統(tǒng)<模塊1>學(xué)習(xí)型模型檢測器輸入：系統(tǒng)模型a+有界線性時態(tài)邏輯公式輸出：用‘經(jīng)典模型檢測算法’判斷‘單個樣本trace’是否滿足‘屬性約束’，得到統(tǒng)計分析樣本Trace分割與特征提取目的：找到一個合適的時間點,使其前段Trace在盡可能短的條件下最大程度地包含對預(yù)測有用的信息,以便SVM預(yù)測后段Trace的信息.思想：條件概率。假設(shè)在A事件發(fā)生的情況下,B事件更有可能發(fā)生,如果P(A)>P(B),則先在模擬Trace的過程中找到A事件的發(fā)生點,在此前提下向后進行多次模擬,以提高捕獲到B事件的可能性.基于屬性約束和隨機行為的特征提取方法：1.確定需要提取的特征變量;2.根據(jù)特征變量提取訓(xùn)練集中Trace的具體特征.

SVM:機器學(xué)習(xí)模型，用于預(yù)測生成新的樣本。如果樣本可信，則使用預(yù)測結(jié)果，并開始下一次模擬；不可信，則進入后段仿真器，模擬出完整的Trace，檢測其結(jié)果。<模塊2>自適應(yīng)統(tǒng)計分析器將<模塊1>的結(jié)果作為統(tǒng)計分析樣本，執(zhí)行統(tǒng)計模型檢測，判定現(xiàn)有樣本是否滿足精度要求，滿足這結(jié)束，否則返回<模塊1>生成更多樣本trace.SPRT順序概率比檢驗；BHT貝葉斯假設(shè)檢驗；BIET貝葉斯區(qū)間估計檢驗。10《面向航天嵌入式軟件的形式化建模方法》研究對象：周期性控制系統(tǒng)的需求獲取、表示、分析驗證方法：模型檢測（分析所建的需求模型）本文思路：航天需求描述語言SPARDL形式化建模方法——用一系列‘模式’來體現(xiàn)嵌入式控制系統(tǒng)的‘行為特征’，每個模式可以周期性地執(zhí)行一系列過程。核心是模式圖，描述模式和模式間的變遷。時序性表示——給出了ITL（基于區(qū)間邏輯的性質(zhì)規(guī)范語言）性質(zhì)模板。從SPARDL自動生成C代碼（給了原理），并快速仿真。實例：某深空探測信號軟件，用于鉆探取土（沒有給出任何數(shù)據(jù)）個人：SPARDL數(shù)用于描述需求的2層語言，上層是模式圖，下層是對應(yīng)的形式化描述。概率模型檢測概率模型檢查把性質(zhì)p在模型的一次執(zhí)行(一條路徑)上是否成立視為一個服從兩項分布的隨機變量.概率模型檢查主要考慮以下兩個問題:給定模型M和性質(zhì)p,

1)估算在模型M的任意一條路徑t上,p成立的可能性,即參數(shù)估計;

2)判斷上述可能性是否大于給定的閾值,即假設(shè)檢驗.

11《同步數(shù)據(jù)流語言高價運算消去的可信翻譯》兩種語言差距較大：Luster*有時鐘同步、數(shù)據(jù)流、并發(fā)及數(shù)據(jù)流對象，其‘變量’和‘表達式’都表示一個‘流數(shù)據(jù)（給定類型的值序列+一個時鐘）’；Clight有順序控制流特征。高階運算：一個對數(shù)組或輸入?yún)?shù)列表進行循環(huán)計算的過程。12《一種基于特征矩陣的軟件脆弱性代碼克隆檢測方法》方法：代碼檢測質(zhì)量：脆弱性（如緩沖區(qū)溢出、內(nèi)存多次釋放、指針誤用等）本文思想：建立一個已發(fā)現(xiàn)的脆弱性代碼數(shù)據(jù)庫,從代碼的相似度層面進行檢測,查找某個軟件系統(tǒng)出現(xiàn)的脆弱性代碼在其他軟件中的分布情況,就可以檢測出更多的脆弱點.提出多類脆弱性檢測模型模型CVdetector實驗數(shù)據(jù)對比10維向量(stmtexp,decl,incr,cond,assign,mul,add,fun_call,fname,fpara)

13《一個及其檢測的Micro-Dalvik虛擬機模型》形式化虛擬機模型，對指令集和運行時狀態(tài)進行了形式化，然后推理證明該虛擬機的正確性。14《信息物理融合系統(tǒng)控制軟件的統(tǒng)計模型檢驗》方法：模型檢測質(zhì)量：系統(tǒng)功能的正確性本文內(nèi)容：基于時間自動機，模塊化描述實時多任務(wù)系統(tǒng)，然后提出一種利用統(tǒng)計模型檢驗技術(shù)，分析系統(tǒng)功能正確性。模型：調(diào)度器、周期性任務(wù)、偶發(fā)任務(wù)、的時間自動機模型。檢測標(biāo)準(zhǔn)：人工分析出