{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:58:59Z","timestamp":1773615539916,"version":"3.50.1"},"reference-count":21,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.3103\/s0146411625700385","type":"journal-article","created":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T19:14:54Z","timestamp":1771528494000},"page":"1105-1124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Exact Schedulability Test for Real-Time Systems with an Abstract Scheduler on Multiprocessor Platforms"],"prefix":"10.3103","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9734-3808","authenticated-orcid":false,"given":"N. O.","family":"Garanina","sequence":"first","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2026,2,19]]},"reference":[{"key":"7898_CR1","volume-title":"Real-Time Systems","author":"J.W.S. Liu","year":"2001","unstructured":"Liu, J.W.S., Real-Time Systems, Prentice-Hall, 2001."},{"key":"7898_CR2","doi-asserted-by":"publisher","unstructured":"Brandenburg, B.B. and G\u00fcl, M., Global scheduling not required: Simple, near-optimal multiprocessor real-time scheduling with semi-partitioned reservations, 2016 IEEE Real-Time Systems Symposium (RTSS), Porto, Portugal, 2016, IEEE, 2016, pp. 99\u2013110. https:\/\/doi.org\/10.1109\/rtss.2016.019","DOI":"10.1109\/rtss.2016.019"},{"key":"7898_CR3","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1109\/tcad.2020.2994265","volume":"40","author":"Q. Zhou","year":"2021","unstructured":"Zhou, Q., Li, G., Zhou, Ch., and Li, J., Limited busy periods in response time analysis for tasks under global EDF scheduling, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 2021, vol. 40, no. 2, pp. 232\u2013245. https:\/\/doi.org\/10.1109\/tcad.2020.2994265","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"7898_CR4","doi-asserted-by":"publisher","unstructured":"Burmyakov, A., Bini, E., and Tovar, E., An exact schedulability test for global FP using state space pruning, Proceedings of the 23rd International Conference on Real Time and Networks Systems, Lille, France, 2015, New York: Association for Computing Machinery, 2015, pp. 225\u2013234. https:\/\/doi.org\/10.1145\/2834848.2834877","DOI":"10.1145\/2834848.2834877"},{"key":"7898_CR5","doi-asserted-by":"publisher","first-page":"2955","DOI":"10.1109\/tc.2022.3142540","volume":"71","author":"A. Burmyakov","year":"2022","unstructured":"Burmyakov, A., Bini, E., and Lee, C.-G., Towards a tractable exact test for global multiprocessor fixed priority scheduling, IEEE Trans. Comput., 2022, vol. 71, no. 11, pp. 2955\u20132967. https:\/\/doi.org\/10.1109\/tc.2022.3142540","journal-title":"IEEE Trans. Comput."},{"key":"7898_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/s11241-023-09398-x","volume":"59","author":"S. Ranjha","year":"2023","unstructured":"Ranjha, S., Gohari, P., Nelissen, G., and Nasri, M., Partial-order reduction in reachability-based response-time analyses of limited-preemptive DAG tasks, Real-Time Syst., 2023, vol. 59, no. 2, pp. 201\u2013255. https:\/\/doi.org\/10.1007\/s11241-023-09398-x","journal-title":"Real-Time Syst."},{"key":"7898_CR7","doi-asserted-by":"publisher","unstructured":"Gohari, P., Voeten, J., and Nasri, M., Reachability-based response-time analysis of preemptive tasks under global scheduling, Proceedings of the 36th Euromicro Conference on Real-Time Systems (ECRTS 2024), Pellizzoni, R., Ed., Leibniz International Proceedings in Informatics, Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, 2024, pp. 3:1\u20133:24. https:\/\/doi.org\/10.4230\/LIPIcs.ECRTS.2024.3","DOI":"10.4230\/LIPIcs.ECRTS.2024.3"},{"key":"7898_CR8","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s11241-015-9245-9","volume":"52","author":"Yo. Sun","year":"2016","unstructured":"Sun, Yo. and Lipari, G., A pre-order relation for exact schedulability test of sporadic tasks on multiprocessor global fixed-priority scheduling, Real-Time Syst., 2016, vol. 52, no. 3, pp. 323\u2013355. https:\/\/doi.org\/10.1007\/s11241-015-9245-9","journal-title":"Real-Time Syst."},{"key":"7898_CR9","doi-asserted-by":"publisher","unstructured":"Cheng, A.M.K., Real-Time Systems: Scheduling, Analysis, and Verification, Wiley, 2002. https:\/\/doi.org\/10.1002\/0471224626","DOI":"10.1002\/0471224626"},{"key":"7898_CR10","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., and Bloem, R., Handbook of Model Checking, Cham: Springer, 2018. https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"7898_CR11","volume-title":"The SPIN Model Checker, Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J., The SPIN Model Checker, Primer and Reference Manual, Reading, MA: Addison-Wesley, 2003."},{"key":"7898_CR12","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., and Tonetta, S., The nuXmv symbolic model checker, Computer Aided Verification. CAV 2014, Biere, A. and Bloem, R., Eds., Lecture Notes in Computer Science, vol. 8559, Cham: Springer, 2014, pp. 334\u2013342. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"7898_CR13","doi-asserted-by":"publisher","unstructured":"Guan, N., Gu, Z., Deng, Q., Gao, Sh., and Yu, G., Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking, Software Technologies for Embedded and Ubiquitous Systems. SEUS 2007, Obermaisser, R., Nah, Y., Puschner, P., and Rammig, F.J., Eds., Lecture Notes in Computer Science, vol. 4761, Berlin: Springer, 2007, pp. 263\u2013272. https:\/\/doi.org\/10.1007\/978-3-540-75664-4_26","DOI":"10.1007\/978-3-540-75664-4_26"},{"key":"7898_CR14","doi-asserted-by":"publisher","unstructured":"Yalcinkaya, B., Nasri, M., and Brandenburg, B.B., An exact schedulability test for non-preemptive self-suspending real-time tasks, 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), Florence, 2019, IEEE, 2019, pp. 1228\u20131233. https:\/\/doi.org\/10.23919\/date.2019.8715111","DOI":"10.23919\/date.2019.8715111"},{"key":"7898_CR15","doi-asserted-by":"publisher","first-page":"49","DOI":"10.15514\/ispras-2020-32(6)-4","volume":"32","author":"S.M. Staroletov","year":"2020","unstructured":"Staroletov, S.M., A formal model of a partitioned real-time operating system in Promela, Trudy Instituta Sistemnogo Programmirovaniya Rossiiskoi Akademii Nauk, 2020, vol. 32, no. 6, pp. 49\u201366. https:\/\/doi.org\/10.15514\/ispras-2020-32(6)-4","journal-title":"Trudy Instituta Sistemnogo Programmirovaniya Rossiiskoi Akademii Nauk"},{"key":"7898_CR16","doi-asserted-by":"publisher","unstructured":"Sukvanich, P., Thongtak, A., and Vatanawood, W., Formalizing real-time embedded system into Promela, MATEC Web Conf., 2015, vol. 35, p. 03003. https:\/\/doi.org\/10.1051\/matecconf\/20153503003","DOI":"10.1051\/matecconf\/20153503003"},{"key":"7898_CR17","doi-asserted-by":"publisher","unstructured":"Geeraerts, G., Goossens, J., and Nguyen, T.-V.-A., A backward algorithm for the multiprocessor online feasibility of sporadic tasks, 2017 17th International Conference on Application of Concurrency to System Design (ACSD), Zaragoza, Spain, 2017, IEEE, 2017, pp. 116\u2013125. https:\/\/doi.org\/10.1109\/acsd.2017.9","DOI":"10.1109\/acsd.2017.9"},{"key":"7898_CR18","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., and Sistla, A.P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst., 1986, vol. 8, no. 2, pp. 244\u2013263. https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7898_CR19","doi-asserted-by":"publisher","first-page":"763","DOI":"10.1007\/s00453-011-9505-6","volume":"63","author":"V. Bonifaci","year":"2010","unstructured":"Bonifaci, V. and Marchetti-Spaccamela, A., Feasibility analysis of sporadic real-time multiprocessor task systems, Algorithmica, 2010, vol. 63, no. 4, pp. 763\u2013780. https:\/\/doi.org\/10.1007\/s00453-011-9505-6","journal-title":"Algorithmica"},{"key":"7898_CR20","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"Hoare, C.A.R., Communicating sequential processes, Commun. ACM, 1978, vol. 21, no. 8, pp. 666\u2013677. https:\/\/doi.org\/10.1145\/359576.359585","journal-title":"Commun. ACM"},{"key":"7898_CR21","doi-asserted-by":"publisher","first-page":"29","DOI":"10.31144\/si.2307-6410.2024.n25.p29-38","volume":"25","author":"N.O. Garanina","year":"2024","unstructured":"Garanina, N.O., An exact schedulability test for real-time systems with an abstract scheduler, Sistemnaya Informatika, 2024, vol. 25, pp. 29\u201338. https:\/\/doi.org\/10.31144\/si.2307-6410.2024.n25.p29-38","journal-title":"Sistemnaya Informatika"}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411625700385.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411625700385","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411625700385.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T22:01:19Z","timestamp":1773612079000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411625700385"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12]]},"references-count":21,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["7898"],"URL":"https:\/\/doi.org\/10.3103\/s0146411625700385","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,12]]},"assertion":[{"value":"6 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 November 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 November 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2026","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The author of this work declares that she has no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}