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

Parameter Generation for Hierarchical Scheduling Systems Based on Model Checking

作　　者：韩朴杰[1] 翟正军[1] 陆艳洪[1] 李运喜[2] HAN Pujie;ZHAI Zhengjun;LU Yanhong;LI Yunxi(School of Computer Science and Engineering, Northwestern Polytechnical University, Xi′an 710072, China;Xi′an Aeronautics Computing Technique Research Institute, AVIC, Xi′an 710068, China)

机构地区：[1]西北工业大学计算机学院,陕西西安710072 [2]航空工业西安航空计算技术研究所,陕西西安710068

出　　处：《西北工业大学学报》2019年第6期1302-1309,共8页Journal of Northwestern Polytechnical University

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

摘　　要：针对综合模块化航空电子(IMA)分级调度系统中的分区参数优化问题,提出了一种基于模型检验的参数生成方法。该方法结合了传统符号模型检验和统计模型检验(SMC)技术,构建一个通用的时间自动机网络来描述分级调度系统的时间行为,在确保系统可调度性的前提下,采用分布式遗传算法搜索具有最优处理器利用率的参数。其中,系统的可调度性约束表述为符号模型检验中的安全性属性和统计模型检验中的假设检验2种形式。相比广泛应用的响应时间分析模型,该方法的形式化模型具有更强的表达能力,能更精确地描述复杂系统特征。而且统计模型检验的引入缓解了传统模型检验的“状态空间爆炸”问题。参数生成实验表明该方法能够定位参数空间中的全局最优解。A parameter generation method based on model checking is proposed to tackle the parameter selection of hierarchical scheduling systems in Integrated Modular Avionics(IMA)by combining the classical symbolic model checking and the Statistical Model Checking(SMC).It builds a generic timed automata network to describe the temporal behavior of hierarchical systems.A distributed genetic algorithm is adopted to search the optimum partition parameters with respect to processor utilization while guaranteeing the schedulability of the system,which is formulated as safety properties of symbolic model checking and hypothesis testing of SMC.Comparing with the widely-used response time analysis,the formal model of this method is more expressive to cover complex features.The application of SMC alleviates the"state space explosion"of classical model checking.Finally,the parameter generation experiments show that the present method is able to find the global optimum solutions in the parameter space.

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

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]