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

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

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

P1Whilex∈Ido

{x:=f(x)}

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

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

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

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

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

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

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