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

论文摘要

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

论文目录

• 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 结 论

文章来源

类型: 期刊论文

作者: 韩朴杰,翟正军,陆艳洪,李运喜

关键词: 综合模块化航电,分级调度,参数生成,时间自动机,统计模型检验,分布式遗传算法

来源: 西北工业大学学报 2019年06期

年度: 2019

分类: 工程科技Ⅱ辑

专业: 航空航天科学与工程

单位: 西北工业大学计算机学院,航空工业西安航空计算技术研究所

基金: 国家自然科学基金(61601371),航空科学基金(2016ZD53035),中航产学研项目(cxy2013XGD14)资助

分类号: V243

页码: 1302-1309

总页数: 8

文件大小: 912K

下载量: 39