針對(duì)綜合模塊化航空電子(IMA)分級(jí)調(diào)度系統(tǒng)中的分區(qū)參數(shù)優(yōu)化問題,提出了一種基于模型檢驗(yàn)的參數(shù)生成方法。該方法結(jié)合了傳統(tǒng)符號(hào)模型檢驗(yàn)和統(tǒng)計(jì)模型檢驗(yàn)(SMC)技術(shù),構(gòu)建一個(gè)通用的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)來(lái)描述分級(jí)調(diào)度系統(tǒng)的時(shí)間行為,在確保系統(tǒng)可調(diào)度性的前提下,采用分布式遺傳算法搜索具有最優(yōu)處理器利用率的參數(shù)。其中,系統(tǒng)的可調(diào)度性約束表述為符號(hào)模型檢驗(yàn)中的安全性屬性和統(tǒng)計(jì)模型檢驗(yàn)中的假設(shè)檢驗(yàn)2種形式。相比廣泛應(yīng)用的響應(yīng)時(shí)間分析模型,該方法的形式化模型具有更強(qiáng)的表達(dá)能力,能更精確地描述復(fù)雜系統(tǒng)特征。而且統(tǒng)計(jì)模型檢驗(yàn)的引入緩解了傳統(tǒng)模型檢驗(yàn)的"狀態(tài)空間爆炸"問題。參數(shù)生成實(shí)驗(yàn)表明該方法能夠定位參數(shù)空間中的全局最優(yōu)解。

【文章頁(yè)數(shù)】：8 頁(yè)

【文章目錄】：
1 問題描述
2 系統(tǒng)建模
    2.1 UPPAAL和時(shí)間自動(dòng)機(jī)
    2.2 模型框架
    2.3 全局調(diào)度器模型
3 參數(shù)生成方法
    3.1 參數(shù)生成流程
    3.2 可調(diào)度性驗(yàn)證
        1) 在UPPAAL SMC的可調(diào)度性測(cè)試中,系統(tǒng)的可調(diào)度性表述為如下的假設(shè)檢驗(yàn)公式:
        2) 當(dāng)執(zhí)行UPPAAL符號(hào)模型檢驗(yàn)時(shí),系統(tǒng)的可調(diào)度性表述為TCTL安全性屬性:
    3.3 處理器利用率的評(píng)估
    3.4 搜索算法的選擇
        1) 初始化:
        2) 劃分:
        3) 交叉:
        4) 變異:
        5) 輸出:
        6) 合并:
        7) 適應(yīng)度計(jì)算:
        8) 選擇:
4 參數(shù)生成實(shí)驗(yàn)
    4.1 實(shí)驗(yàn)方案
        1) 實(shí)驗(yàn)1:
        2) 實(shí)驗(yàn)2:
    4.2 結(jié)果分析
5 結(jié) 論



本文編號(hào)：3777946