Issue |
JNWPU
Volume 37, Number 6, December 2019
|
|
---|---|---|
Page(s) | 1302 - 1309 | |
DOI | https://doi.org/10.1051/jnwpu/20193761302 | |
Published online | 11 February 2020 |
Parameter Generation for Hierarchical Scheduling Systems Based on Model Checking
基于模型检验的分级调度系统参数生成方法
1
School of Computer Science and Engineering, Northwestern Polytechnical University, Xi'an 710072, China
2
Xi'an Aeronautics Computing Technique Research Institute, AVIC, Xi'an 710068, China
Received:
21
December
2018
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.
摘要
针对综合模块化航空电子(IMA)分级调度系统中的分区参数优化问题,提出了一种基于模型检验的参数生成方法。该方法结合了传统符号模型检验和统计模型检验(SMC)技术,构建一个通用的时间自动机网络来描述分级调度系统的时间行为,在确保系统可调度性的前提下,采用分布式遗传算法搜索具有最优处理器利用率的参数。其中,系统的可调度性约束表述为符号模型检验中的安全性属性和统计模型检验中的假设检验2种形式。相比广泛应用的响应时间分析模型,该方法的形式化模型具有更强的表达能力,能更精确地描述复杂系统特征。而且统计模型检验的引入缓解了传统模型检验的"状态空间爆炸"问题。参数生成实验表明该方法能够定位参数空间中的全局最优解。
Key words: integrated modular avionics / hierarchical scheduling / parameter generation / timed automata / statistical model checking / distributed genetic algorithm
关键字 : 综合模块化航电 / 分级调度 / 参数生成 / 时间自动机 / 统计模型检验 / 分布式遗传算法
© 2019 Journal of Northwestern Polytechnical University. All rights reserved.
This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.