{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:51:39Z","timestamp":1772164299412,"version":"3.50.1"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,2,7]],"date-time":"2021-02-07T00:00:00Z","timestamp":1612656000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,2,7]],"date-time":"2021-02-07T00:00:00Z","timestamp":1612656000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/s10009-020-00597-6","type":"journal-article","created":{"date-parts":[[2021,2,9]],"date-time":"2021-02-09T03:20:09Z","timestamp":1612840809000},"page":"721-740","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Model-based optimization of ARINC-653 partition scheduling"],"prefix":"10.1007","volume":"23","author":[{"given":"Pujie","family":"Han","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhengjun","family":"Zhai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"Nielsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrik","family":"Nyman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,2,7]]},"reference":[{"key":"597_CR1","unstructured":"AEEC: Avionics application software standard interface: Part 1\u2014required services. ARINC specification 653P1-4, Aeronautical Radio Inc. (2015)"},{"issue":"1","key":"597_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1162\/evco.1993.1.1.1","volume":"1","author":"T B\u00e4ck","year":"1993","unstructured":"B\u00e4ck, T., Schwefel, H.P.: An overview of evolutionary algorithms for parameter optimization. Evol. Comput. 1(1), 1\u201323 (1993)","journal-title":"Evol. Comput."},{"key":"597_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Formal methods for the design of real-time systems, pp. 200\u2013236. Springer, New York (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"597_CR4","doi-asserted-by":"crossref","unstructured":"Beji, S., Hamadou, S., Gherbi, A., Mullins, J.: Smt-based cost optimization approach for the integration of avionic functions in IMA and TTEthernet architectures. In: Proceedings of the 2014 IEEE\/ACM 18th International Symposium on Distributed Simulation and Real Time Applications, pp. 165\u2013174. IEEE Computer Society (2014)","DOI":"10.1109\/DS-RT.2014.28"},{"issue":"1","key":"597_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0303-2647(96)01657-7","volume":"41","author":"HG Beyer","year":"1997","unstructured":"Beyer, H.G.: An alternative explanation for the manner in which genetic algorithms operate. Biosystems 41(1), 1\u201315 (1997)","journal-title":"Biosystems"},{"issue":"1","key":"597_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1015059928466","volume":"1","author":"HG Beyer","year":"2002","unstructured":"Beyer, H.G., Schwefel, H.P.: Evolution strategies\u2014a comprehensive introduction. Nat. Comput. 1(1), 3\u201352 (2002)","journal-title":"Nat. Comput."},{"issue":"4","key":"597_CR7","doi-asserted-by":"publisher","first-page":"977","DOI":"10.1007\/s11081-018-9385-6","volume":"19","author":"M Blikstad","year":"2018","unstructured":"Blikstad, M., Karlsson, E., L\u00f6\u00f6w, T., R\u00f6nnberg, E.: An optimisation approach for pre-runtime scheduling of tasks and communication in an integrated modular avionic system. Optim. Eng. 19(4), 977\u20131004 (2018)","journal-title":"Optim. Eng."},{"key":"597_CR8","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.scico.2016.05.008","volume":"127","author":"A Boudjadar","year":"2016","unstructured":"Boudjadar, A., David, A., Kim, J.H., Larsen, K.G., Miku\u010dionis, M., Nyman, U., Skou, A.: Statistical and exact schedulability analysis of hierarchical scheduling systems. Sci. Comput. Program. 127, 103\u2013130 (2016)","journal-title":"Sci. Comput. Program."},{"key":"597_CR9","unstructured":"Boudjadar, J., David, A., Kim, J.H., Larsen, K.G., Nyman, U., Skou, A.: Schedulability and energy efficiency for multi-core hierarchical scheduling systems. In: Embedded Real Time Systems and Software pp. 1\u20134 (2014)"},{"key":"597_CR10","unstructured":"Boudjadar, J., Larsen, K.G., Kim, J.H., Nyman, U.: Compositional schedulability analysis of an avionics system using UPPAAL. In: AASE 2014"},{"issue":"5","key":"597_CR11","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1109\/TSE.2012.54","volume":"39","author":"L Carnevali","year":"2013","unstructured":"Carnevali, L., Pinzuti, A., Vicario, E.: Compositional verification for hierarchical scheduling of real-time systems. IEEE Trans. Software Eng. 39(5), 638\u2013657 (2013)","journal-title":"IEEE Trans. Software Eng."},{"issue":"4","key":"597_CR12","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transfer 17(4), 397\u2013415 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"597_CR13","unstructured":"Davis, R., Burns, A.: An investigation into server parameter selection for hierarchical fixed priority pre-emptive systems. In: 16th International Conference on Real-Time and Network Systems (RTNS 2008) (2008)"},{"key":"597_CR14","doi-asserted-by":"crossref","unstructured":"Dewan, F., Fisher, N.: Approximate bandwidth allocation for fixed-priority-scheduled periodic resources. In: 2010 16th IEEE Real-Time and Embedded Technology and Applications Symposium, pp. 247\u2013256. IEEE (2010)","DOI":"10.1109\/RTAS.2010.28"},{"key":"597_CR15","doi-asserted-by":"crossref","unstructured":"Easwaran, A., Anand, M., Lee, I.: Compositional analysis framework using EDP resource models. In: 28th IEEE International Real-Time Systems Symposium (RTSS 2007), pp. 129\u2013138. IEEE (2007)","DOI":"10.1109\/RTSS.2007.36"},{"key":"597_CR16","doi-asserted-by":"crossref","unstructured":"Easwaran, A., Lee, I., Sokolsky, O., Vestal, S.: A compositional scheduling framework for digital avionics systems. In: ERCSA 2009","DOI":"10.1109\/RTCSA.2009.46"},{"key":"597_CR17","unstructured":"Freiberg, P.S., Krag, J.M., Villumsen, B.: Distributed parameter sweep for Uppaal models. Ph.D. thesis, Aalborg University (2011)"},{"key":"597_CR18","doi-asserted-by":"crossref","unstructured":"Han, P., Zhai, Z., Nielsen, B., Nyman, U.: A modeling framework for schedulability analysis of distributed avionics systems. In: 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018, pp. 150\u2013168. EPTCS (2018)","DOI":"10.4204\/EPTCS.268.5"},{"key":"597_CR19","doi-asserted-by":"crossref","unstructured":"Han, P., Zhai, Z., Nielsen, B., Nyman, U.M.: A compositional approach for schedulability analysis of distributed avionics systems. In: International Workshop on Methods and Tools for Rigorous System Design, pp. 39\u201351 (2018)","DOI":"10.4204\/EPTCS.272.4"},{"key":"597_CR20","doi-asserted-by":"crossref","unstructured":"Kelly, O.R., Aydin, H., Zhao, B.: On partitioned scheduling of fixed-priority mixed-criticality task sets. In: 2011 IEEE 10th International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom), pp. 1051\u20131059. IEEE (2011)","DOI":"10.1109\/TrustCom.2011.144"},{"key":"597_CR21","doi-asserted-by":"crossref","unstructured":"Kim, J.E., Abdelzaher, T., Sha, L.: Schedulability bound for integrated modular avionics partitions. In: Proceedings of the 2015 Design, Automation and Test in Europe Conference and Exhibition, pp. 37\u201342. EDA Consortium (2015)","DOI":"10.7873\/DATE.2015.1026"},{"issue":"3","key":"597_CR22","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1145\/2983185.2983192","volume":"13","author":"JH Kim","year":"2016","unstructured":"Kim, J.H., Legay, A., Traonouez, L.M., Boudjadar, A., Nyman, U., Larsen, K.G., Lee, I., Choi, J.Y.: Optimizing the resource requirements of hierarchical scheduling systems. ACM Sigbed Rev. 13(3), 41\u201348 (2016)","journal-title":"ACM Sigbed Rev."},{"issue":"2","key":"597_CR23","first-page":"257","volume":"1","author":"G Lipari","year":"2005","unstructured":"Lipari, G., Bini, E.: A methodology for designing hierarchical scheduling systems. J. Embed. Comput. 1(2), 257\u2013269 (2005)","journal-title":"J. Embed. Comput."},{"key":"597_CR24","doi-asserted-by":"crossref","unstructured":"Mendoza, L.E., Capel, M.I., P\u00e9rez, M., Benghazi, K.: Compositional model-checking verification of critical systems. In: International Conference on Enterprise Information Systems, pp. 213\u2013225. Springer, Berlin (2008)","DOI":"10.1007\/978-3-642-00670-8_16"},{"issue":"1","key":"597_CR25","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1162\/evco.1993.1.1.25","volume":"1","author":"H M\u00fchlenbein","year":"1993","unstructured":"M\u00fchlenbein, H., Schlierkamp-Voosen, D.: Predictive models for the breeder genetic algorithm I. Continuous parameter optimization. Evolut. Comput. 1(1), 25\u201349 (1993)","journal-title":"Evolut. Comput."},{"key":"597_CR26","doi-asserted-by":"crossref","unstructured":"M\u00fchlenbein, H., Voigt, H.M.: Gene pool recombination in genetic algorithms. In: Meta-Heuristics, pp. 53\u201362. Springer, Berlin (1996)","DOI":"10.1007\/978-1-4613-1361-8_4"},{"key":"597_CR27","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: CAV, vol. 3114, pp. 202\u2013215. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"597_CR28","unstructured":"Shin, I., Lee, I.: Compositional real-time scheduling framework. In: 25th IEEE International on Real-Time Systems Symposium, 2004. Proceedings. pp. 57\u201367. IEEE (2004)"},{"issue":"3","key":"597_CR29","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/1347375.1347383","volume":"7","author":"I Shin","year":"2008","unstructured":"Shin, I., Lee, I.: Compositional real-time scheduling framework with periodic model. ACM Transactions on Embedded Computing Systems (TECS) 7(3), 30 (2008)","journal-title":"ACM Transactions on Embedded Computing Systems (TECS)"},{"key":"597_CR30","doi-asserted-by":"crossref","unstructured":"Shukla, A., Pandey, H.M., Mehrotra, D.: Comparative review of selection techniques in genetic algorithm. In: 2015 International Conference on Futuristic Trends on Computational Analysis and Knowledge Management (ABLAZE), pp. 515\u2013519. IEEE (2015)","DOI":"10.1109\/ABLAZE.2015.7154916"},{"key":"597_CR31","volume-title":"Evolutionary Intelligence: An Introduction to Theory and Applications with Matlab","author":"S Sumathi","year":"2008","unstructured":"Sumathi, S., Hamsapriya, T., Surekha, P.: Evolutionary Intelligence: An Introduction to Theory and Applications with Matlab. Springer, New York (2008)"},{"key":"597_CR32","doi-asserted-by":"crossref","unstructured":"Sun, Y., Lipari, G., Soulat, R., Fribourg, L., Markey, N.: Component-based analysis of hierarchical scheduling using linear hybrid automata. In: ERCSA 2014","DOI":"10.1109\/RTCSA.2014.6910502"},{"key":"597_CR33","doi-asserted-by":"crossref","unstructured":"Yoon, M.K., Kim, J.E., Bradford, R., Sha, L.: Holistic design parameter optimization of multiple periodic resources in hierarchical scheduling. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 1313\u20131318. EDA Consortium (2013)","DOI":"10.7873\/DATE.2013.271"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00597-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00597-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00597-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,26]],"date-time":"2021-11-26T12:05:36Z","timestamp":1637928336000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00597-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,7]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["597"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00597-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,7]]},"assertion":[{"value":"1 December 2020","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 February 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}