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