一、研究目標(biāo)針對嵌入式操作系統(tǒng)行為交互復(fù)雜、代碼量大導(dǎo)致的形式化建模困難、形式化驗(yàn)證效率低和驗(yàn)證不充分的問題，突破復(fù)雜系統(tǒng)的組合建模驗(yàn)證和自動(dòng)化驗(yàn)證等關(guān)鍵技術(shù)，研發(fā)相應(yīng)的形式化驗(yàn)證工具。在保證驗(yàn)證質(zhì)量的前提下，降低操作系統(tǒng)的驗(yàn)證復(fù)雜度、提高驗(yàn)證效率，為操作系統(tǒng)從行為屬性端到設(shè)計(jì)實(shí)現(xiàn)端的整體自動(dòng)形式化驗(yàn)證奠定技術(shù)基礎(chǔ)。二、主要研究內(nèi)容（）開展嵌入式操作系統(tǒng)關(guān)鍵模塊組合建模驗(yàn)證技術(shù)研究，解決復(fù)雜驗(yàn)證目標(biāo)因不變量集聚而導(dǎo)致的驗(yàn)證復(fù)雜度高、驗(yàn)證不充分問題；（）開展嵌入式操作系統(tǒng)關(guān)鍵模塊自動(dòng)形式化驗(yàn)證技術(shù)研究，解決關(guān)鍵系統(tǒng)模塊自動(dòng)化驗(yàn)證中存在的并發(fā)隨機(jī)行為難仿真、需求屬性難度量等痛點(diǎn)問題，實(shí)現(xiàn)系統(tǒng)任意行為的精確描述仿真和高效自動(dòng)化驗(yàn)證。（）開展嵌入式操作系統(tǒng)多線程并發(fā)行為的形式化建模與驗(yàn)證技術(shù)研究，驗(yàn)證并發(fā)場景下系統(tǒng)易出現(xiàn)的死鎖、內(nèi)存資源泄露等安全問題。三、指標(biāo)（）實(shí)現(xiàn)嵌入式操作系統(tǒng)關(guān)鍵模塊抽象行為形式化建模，支持嵌入式系統(tǒng)隨機(jī)交互事件行為仿真；（）提供需求與設(shè)計(jì)實(shí)現(xiàn)的一致性自動(dòng)化驗(yàn)證，支持定性屬性自動(dòng)形式化驗(yàn)證（如，自動(dòng)判定系統(tǒng)滿足特定需求規(guī)范的概率是否大于或等于某一閾值），支持定量屬性形式化驗(yàn)證（如，自動(dòng)統(tǒng)計(jì)出系統(tǒng)滿足特定需求規(guī)范的概率）；（）支持嵌入式操作系統(tǒng)關(guān)鍵模塊的死鎖、資源泄露等高危漏洞挖掘；（）支持自動(dòng)化參數(shù)探索的批量屬性形式化驗(yàn)證、驗(yàn)證結(jié)果統(tǒng)計(jì)及可視化。四、線下對接方式本課題采用線下對接報(bào)名。聯(lián)系人：姚蕊聯(lián)系電話：/-聯(lián)系郵箱：@.項(xiàng)目詳情：操作系統(tǒng)關(guān)鍵模塊形式化驗(yàn)證方法研究