Back to Search
Start Over
Model-based optimization of ARINC-653 partition scheduling
- Source :
- Han, P, Zhai, Z, Nielsen, B & Nyman, U 2021, ' Model-based optimization of ARINC-653 partition scheduling ', International Journal on Software Tools for Technology Transfer, vol. 23, no. 5, pp. 721-740 . https://doi.org/10.1007/s10009-020-00597-6
- Publication Year :
- 2021
- Publisher :
- Springer Science and Business Media LLC, 2021.
-
Abstract
- The architecture of ARINC-653 partitioned scheduling has been widely applied to avionics systems owing to its robust temporal isolation among applications. However, this partitioning mechanism causes the problem of how to optimize the partition scheduling of a complex system while guaranteeing its schedulability. In this paper, a model-based optimization approach is proposed. We formulate the problem as a parameter sweep application, which searches for the optimal partition scheduling parameters with respect to minimum processor occupancy via an evolutionary algorithm. An ARINC-653 partitioned scheduling system is modeled as a set of timed automata in the model checker UPPAAL. The optimizer tentatively assigns parameter settings to the models and subsequently invokes UPPAAL to verify schedulability as well as evaluate promising solutions. The parameter space is explored with an evolutionary algorithm that combines refined genetic operators and the self-adaptation of evolution strategies. The experimental results show the applicability of our optimization method. The architecture of ARINC-653 partitioned scheduling has been widely applied to avionics systems owing to its robust temporal isolation among applications. However, this partitioning mechanism causes the problem of how to optimize the partition scheduling of a complex system while guaranteeing its schedulability. In this paper, a model-based optimization approach is proposed. We formulate the problem as a parameter sweep application, which searches for the optimal partition scheduling parameters with respect to minimum processor occupancy via an evolutionary algorithm. An ARINC-653 partitioned scheduling system is modeled as a set of timed automata in the model checker UPPAAL. The optimizer tentatively assigns parameter settings to the models and subsequently invokes UPPAAL to verify schedulability as well as evaluate promising solutions. The parameter space is explored with an evolutionary algorithm that combines refined genetic operators and the self-adaptation of evolution strategies. The experimental results show the applicability of our optimization method.
- Subjects :
- Model checking
Mathematical optimization
Computer science
Evolutionary algorithm
Scheduling (production processes)
020207 software engineering
02 engineering and technology
Parameter space
Partition (database)
UPPAAL
020202 computer hardware & architecture
Automaton
Model-based optimization
Partitioned scheduling
ARINC 653
Theory of computation
0202 electrical engineering, electronic engineering, information engineering
Timed automata
Computer Science::Operating Systems
Software
Parameter sweep
Information Systems
Subjects
Details
- ISSN :
- 14332787 and 14332779
- Volume :
- 23
- Database :
- OpenAIRE
- Journal :
- International Journal on Software Tools for Technology Transfer
- Accession number :
- edsair.doi.dedup.....2aee46265c1022e8ed2ee6bc234fa46e