基于模型检验的分级调度系统参数生成方法

发布时间：2023-04-01 22:05

　　针对综合模块化航空电子(IMA)分级调度系统中的分区参数优化问题,提出了一种基于模型检验的参数生成方法。该方法结合了传统符号模型检验和统计模型检验(SMC)技术,构建一个通用的时间自动机网络来描述分级调度系统的时间行为,在确保系统可调度性的前提下,采用分布式遗传算法搜索具有最优处理器利用率的参数。其中,系统的可调度性约束表述为符号模型检验中的安全性属性和统计模型检验中的假设检验2种形式。相比广泛应用的响应时间分析模型,该方法的形式化模型具有更强的表达能力,能更精确地描述复杂系统特征。而且统计模型检验的引入缓解了传统模型检验的"状态空间爆炸"问题。参数生成实验表明该方法能够定位参数空间中的全局最优解。

【文章页数】：8 页

【文章目录】：
1 问题描述
2 系统建模
    2.1 UPPAAL和时间自动机
    2.2 模型框架
    2.3 全局调度器模型
3 参数生成方法
    3.1 参数生成流程
    3.2 可调度性验证
        1) 在UPPAAL SMC的可调度性测试中,系统的可调度性表述为如下的假设检验公式:
        2) 当执行UPPAAL符号模型检验时,系统的可调度性表述为TCTL安全性属性:
    3.3 处理器利用率的评估
    3.4 搜索算法的选择
        1) 初始化:
        2) 划分:
        3) 交叉:
        4) 变异:
        5) 输出:
        6) 合并:
        7) 适应度计算:
        8) 选择:
4 参数生成实验
    4.1 实验方案
        1) 实验1:
        2) 实验2:
    4.2 结果分析
5 结 论



本文编号：3777946