面向安全關(guān)鍵內(nèi)存管理系統(tǒng)分層驗(yàn)證方法

摘要： 安全關(guān)鍵系統(tǒng)的失敗會造成很嚴(yán)重的后果,確保其正確性非常重要.空間嵌入式操作系統(tǒng)是一個(gè)典型的安全關(guān)鍵系統(tǒng),在其內(nèi)存管理的設(shè)計(jì)上,必須保障其高效的分配與回收,同時(shí)對系統(tǒng)資源的占用降到最低.在傳統(tǒng)的軟件開發(fā)過程中,通常是在整個(gè)軟件開發(fā)結(jié)束后再進(jìn)行集中測試及驗(yàn)證,這樣勢必會造成開發(fā)進(jìn)展的不確定性.因此,將形式化驗(yàn)證方法和軟件工程領(lǐng)域內(nèi)的“需求-設(shè)計(jì)-實(shí)現(xiàn)”的3層開發(fā)框架相結(jié)合,通過性質(zhì)...