|
|
论文:2019,Vol:37,Issue(6):1302-1309 |
|
|
引用本文： |
|
|
韩朴杰, 翟正军, 陆艳洪, 李运喜. 基于模型检验的分级调度系统参数生成方法[J]. 西北工业大学学报 |
|
|
HAN Pujie, ZHAI Zhengjun, LU Yanhong, LI Yunxi. Parameter Generation for Hierarchical Scheduling Systems Based on Model Checking[J]. Northwestern polytechnical university |
|
|
|
|
|
|
|
| 基于模型检验的分级调度系统参数生成方法 |
|
| 韩朴杰1, 翟正军1, 陆艳洪1, 李运喜2 |
|
1. 西北工业大学 计算机学院, 陕西 西安 710072;
2. 航空工业 西安航空计算技术研究所, 陕西 西安 710068 |
| 摘要: |
| 针对综合模块化航空电子（IMA）分级调度系统中的分区参数优化问题，提出了一种基于模型检验的参数生成方法。该方法结合了传统符号模型检验和统计模型检验（SMC）技术，构建一个通用的时间自动机网络来描述分级调度系统的时间行为，在确保系统可调度性的前提下，采用分布式遗传算法搜索具有最优处理器利用率的参数。其中，系统的可调度性约束表述为符号模型检验中的安全性属性和统计模型检验中的假设检验2种形式。相比广泛应用的响应时间分析模型，该方法的形式化模型具有更强的表达能力，能更精确地描述复杂系统特征。而且统计模型检验的引入缓解了传统模型检验的"状态空间爆炸"问题。参数生成实验表明该方法能够定位参数空间中的全局最优解。 |
| 关键词:
综合模块化航电
分级调度
参数生成
时间自动机
统计模型检验
分布式遗传算法
|
|
| Parameter Generation for Hierarchical Scheduling Systems Based on Model Checking |
|
| HAN Pujie1, ZHAI Zhengjun1, LU Yanhong1, LI Yunxi2 |
|
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 |
| Abstract: |
| 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. |
| Key words:
integrated modular avionics
hierarchical scheduling
parameter generation
timed automata
statistical model checking
distributed genetic algorithm
|
|
| 收稿日期: 2018-12-21
修回日期:
|
| DOI: 10.1051/jnwpu/20193761302 |
| 基金项目: 国家自然科学基金（61601371）、航空科学基金（2016ZD53035）与中航产学研项目（cxy2013XGD14）资助 |
| 通讯作者:
Email： |
| 作者简介: 韩朴杰(1988-),西北工业大学博士研究生,主要从事嵌入式计算系统和软件形式化方法研究。
|
|
|
|
|
|
|
|
参考文献: |
|
|
[1] BLIKSTAD M, KARLSSON E, LÖÖW T, et al. An Optimisation Approach for Pre-Runtime Scheduling of Tasks and Communication in an Integrated Modular Avionic System[J]. Optimization and Engineering, 2018, 19(4):977-1004
[2] Airlines Electronic Engineering Committee. Avionics Application Software Standard Interface:Part 1-Required Services[S]. ARINC Specification 653 P1-4, 2015
[3] CARNEVALI L, PINZUTI A, VICARIO E. Compositional Verification for Hierarchical Scheduling of Real-Time Systems[J]. IEEE Trans on Software Engineering, 2013, 39(5):638-657
[4] KIM J E, ABDELZAHER T, SHA L. Schedulability Bound for Integrated Modular Avionics Partitions[C]//Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2015:37-42
[5] SHIN I, LEE I. Periodic Resource Model for Compositional Real-Time Guarantees[C]//Real-Time Systems Symposium, 2003:2-13
[6] LIPARI G, BINI E. A Methodology for Designing Hierarchical Scheduling Systems[J]. Journal of Embedded Computing, 2005, 1(2):257-269
[7] ALMEIDA L, PEDREIRAS P. Scheduling within Temporal Partitions:Response-Time Analysis and Server Design[C]//Proceedings of the 4th ACM International Conference on Embedded Software, 2004:95-103
[8] ZHANG L, GOSWAMI D, SCHNEIDER R, et al. Task-and Network-Level Schedule Co-Synthesis of Ethernet-Based Time-Triggered Systems[C]//19th Asia and South Pacific Design Automation Conference, 2014:119-124
[9] YOON M K, KIM J E, BRADFORD R, et al. Holistic Design Parameter Optimization of Multiple Periodic Resources in Hierarchical Scheduling[C]//Proceedings of the Conference on Design, Automation and Test in Europe, 2013:1313-1318
[10] DAVIS R, BURNS A. An Investigation into Server Parameter Selection for Hierarchical Fixed Priority Pre-Emptive Systems[C]//16th International Conference on Real-Time and Network Systems, 2008
[11] DEWAN F, FISHER N. Approximate Bandwidth Allocation for Fixed-Priority-Scheduled Periodic Resources[C]//Real-Time and Embedded Technology and Applications Symposium, 2010:247-256
[12] DEWAN F, FISHER N. Fixed-Priority Schedulability of Arbitrary-Deadline Sporadic Tasks upon Periodic Resources[C]//IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, 2012:358-367
[13] BEJI S, HAMADOU S, GHERBI A, et al. SMT-Based Cost Optimization Approach for the Integration of Avionic Functions in IMA and TT Ethernet Architectures[C]//Proceedings of the 2014 IEEE/ACM 18th International Symposium on Distributed Simulation and Real Time Applications, 2014:165-174
[14] CARNEVALI L, LIPARI G, PINZUTI A, et al. A Formal Approach to Design and Verification of Two-Level Hierarchical Scheduling Systems[C]//International Conference on Reliable Software Technologies, 2011:118-131
[15] CICIRELLI F, FURFARO A, NIGRO L, et al. Development of a Schedulability Analysis Framework Based on PTPN and UPPAAL with Stopwatches[C]//Proceedings of the 2012 IEEE/ACM 16th International Symposium on Distributed Simulation and Real Time Applications, 2012:57-64
[16] SUN Y, LIPARI G, SOULAT R, et al. Component-Based Analysis of Hierarchical Scheduling Using Linear Hybrid Automata[C]//20th International Conference on Embedded and Real-Time Computing Systems and Applications, 2014:1-10
[17] SBERG M, PETTERSSON P, NOLTE T. Modelling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling[C]//23rd Euromicro Conference on Real-Time Systems, 2011:172-181
[18] AHN S J, HWANG D Y, KANG M, et al. Hierarchical System Schedulability Analysis Framework Using UPPAAL[J]. IEICE Transactions on Information and Systems, 2016, 99(8):2172-2176
[19] HAN P, ZHAI Z, NIELSEN B, et al. A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems[C]//International Workshop on Methods and Tools for Rigorous System Design, 2018:39-51
[20] BOUDJADAR A, KIM J H, LARSEN K G, et al. Compositional Schedulability Analysis of An Avionics System Using UPPAAL[C]//International Conference on Advanced Aspeots of Softuare Engineering, 2014:140-147
[21] PELED D A. Software Reliability Methods[M]. New York:Springer Science & Business Media, 2013
[22] UPPSALA University, AALBORG University. UPPAAL Home[EB/OL]. (2015-6-2)[2018-7-1]. http://www.uppaal.org/.
[23] DAVID A, LARSEN K G, LEGAY A, et al. UPPAAL SMC Tutorial[J]. International Journal on Software Tools for Technology Transfer, 2015, 17(4):397-415
[24] DAVID G B A, LARSEN K G. A Tutorial on UPPAAL 4.0[J]. Department of Computer Science, 2006, 4(12):200-236
[25] BÄCK T, FOGEL D B, MICHALEWICZ T. Evolutionary Computeation 1:Basic Algorithns and Operators[M]. New York:CRC Press, 2018 |
|
|
|
|
|
|
|
