{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:42Z","timestamp":1759638942795,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T00:00:00Z","timestamp":1531785600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Comb Optim"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10878-018-0328-0","type":"journal-article","created":{"date-parts":[[2018,7,17]],"date-time":"2018-07-17T05:08:01Z","timestamp":1531804081000},"page":"901-920","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verifying schedulability of tasks in ROS-based systems"],"prefix":"10.1007","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2772-1433","authenticated-orcid":false,"given":"Jin","family":"Cui","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongwei","family":"Du","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,17]]},"reference":[{"key":"328_CR1","doi-asserted-by":"crossref","unstructured":"Alur R (1999) Timed automata. In: International conference on computer aided verification. Springer, pp 8\u201322","DOI":"10.1007\/3-540-48683-6_3"},{"issue":"1","key":"328_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill D (1993) Model-checking in dense real-time. Inf Comput 104(1):2\u201334","journal-title":"Inf Comput"},{"key":"328_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann G, David A, Larsen KG (2004) A tutorial on uppaal. In: Formal methods for the design of real-time systems. Springer, Berlin, pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"issue":"4","key":"328_CR4","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1109\/TASE.2010.2050199","volume":"7","author":"H Bel Mokadem","year":"2010","unstructured":"Bel Mokadem H, Berard B, Gourcuff V, De Smet O, Roussel JM (2010) Verification of a timed multitask system with UPPAAL. IEEE Trans Autom Sci Eng 7(4):921\u2013932","journal-title":"IEEE Trans Autom Sci Eng"},{"issue":"11","key":"328_CR5","doi-asserted-by":"publisher","first-page":"1462","DOI":"10.1109\/TC.2004.103","volume":"53","author":"E Bini","year":"2004","unstructured":"Bini E, Buttazzo GC (2004) Schedulability analysis of periodic fixed priority systems. IEEE Trans Comput 53(11):1462\u20131473","journal-title":"IEEE Trans Comput"},{"issue":"7","key":"328_CR6","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1109\/TC.2003.1214341","volume":"52","author":"E Bini","year":"2003","unstructured":"Bini E, Buttazzo GC, Buttazzo GM (2003) Rate monotonic analysis: the hyperbolic bound. IEEE Trans Comput 52(7):933\u2013942","journal-title":"IEEE Trans Comput"},{"issue":"2","key":"328_CR7","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1109\/TSE.2004.1265815","volume":"30","author":"G Bucci","year":"2004","unstructured":"Bucci G, Fedeli A, Sassoli L, Vicario E (2004) Timed state space analysis of real-time preemptive systems. IEEE Trans Softw Eng 30(2):97\u2013111","journal-title":"IEEE Trans Softw Eng"},{"issue":"2","key":"328_CR8","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1109\/TR.2018.2806349","volume":"67","author":"J Cui","year":"2018","unstructured":"Cui J, Duan Z, Tian C, Du H, Zhang N (2018) A novel approach to modeling and verifying real-time systems for high reliability. IEEE Trans Reliab 67(2):481\u2013493","journal-title":"IEEE Trans Reliab"},{"issue":"6","key":"328_CR9","first-page":"1670","volume":"29","author":"J Cui","year":"2018","unstructured":"Cui J, Duan Z, Tian C, Zhang N (2018) Modeling and analysis of nested interrupt systems. J Softw 29(6):1670\u20131680 (in Chinese)","journal-title":"J Softw"},{"key":"328_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.robot.2015.11.012","volume":"77","author":"L Dennis","year":"2016","unstructured":"Dennis L, Fisher M, Slavkovik M, Webster M (2016) Formal verification of ethical choices in autonomous systems. Robot Auton Syst 77:1\u201314","journal-title":"Robot Auton Syst"},{"key":"328_CR11","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.tcs.2014.02.011","volume":"554","author":"Z Duan","year":"2014","unstructured":"Duan Z, Tian C (2014) A practical decision procedure for propositional projection temporal logic with infinite models. Theor Comput Sci 554:169\u2013190","journal-title":"Theor Comput Sci"},{"key":"328_CR12","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1016\/j.tcs.2015.08.039","volume":"609","author":"Z Duan","year":"2016","unstructured":"Duan Z, Tian C, Zhang N (2016) A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor Comput Sci 609:544\u2013560","journal-title":"Theor Comput Sci"},{"key":"328_CR13","volume-title":"Principles of model checking","author":"JS Katoen","year":"2008","unstructured":"Katoen JS (2008) Principles of model checking. The MIT Press, Cambridge"},{"key":"328_CR14","doi-asserted-by":"crossref","unstructured":"Kortenkamp D, Simmons R, Brugali D (2016) Robotic systems architectures and programming. In: Springer Handbook of Robotics. Springer, Berlin, pp 283\u2013306","DOI":"10.1007\/978-3-319-32552-1_12"},{"key":"328_CR15","unstructured":"Labrosse JJ (2009) uC\/OS-III, The real-time kernel. Micrium Press, Texas"},{"issue":"1","key":"328_CR16","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/321738.321743","volume":"20","author":"CL Liu","year":"1973","unstructured":"Liu CL, Layland JW (1973) Scheduling algorithms for multiprogramming in a hard-real-time environment. JACM 20(1):46\u201361","journal-title":"JACM"},{"issue":"4","key":"328_CR17","doi-asserted-by":"publisher","first-page":"3239","DOI":"10.1109\/TIE.2016.2633476","volume":"64","author":"J Liu","year":"2017","unstructured":"Liu J, Zhou M, Song X, Gu M, Sun J (2017) Formal modeling and verification of a rate-monotonic scheduling implementation with real-time maude. IEEE Trans Ind Electron 64(4):3239\u20133249","journal-title":"IEEE Trans Ind Electron"},{"issue":"12","key":"328_CR18","doi-asserted-by":"publisher","first-page":"1312","DOI":"10.1177\/0278364917733549","volume":"36","author":"S Mitsch","year":"2017","unstructured":"Mitsch S, Ghorbal K, Vogelbacher D, Platzer A (2017) Formal verification of obstacle avoidance and navigation of ground robots. Int J Robot Res 36(12):1312\u20131340","journal-title":"Int J Robot Res"},{"issue":"3","key":"328_CR19","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/2984450.2984459","volume":"3","author":"CA Munoz","year":"2016","unstructured":"Munoz CA, Dutle A, Narkawicz A, Upchurch J (2016) Unmanned aircraft systems in the national airspace system: a formal methods perspective. ACM SIGLOG News 3(3):67\u201376","journal-title":"ACM SIGLOG News"},{"key":"328_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlamp.2017.07.001","volume":"92","author":"J Park","year":"2017","unstructured":"Park J, Lee I, Sokolsky O, Hwang DY, Ahn S, Choi JY, Kang I (2017) A process algebraic approach to the schedulability analysis and workload abstraction of hierarchical real-time systems. J Log Algebraic Methods Program 92:1\u201318","journal-title":"J Log Algebraic Methods Program"},{"key":"328_CR21","unstructured":"Quigley M, Conley K, Gerkey B, Faust J, Foote T, Leibs J, Wheeler R, Ng AY (2009) ROS: an open-source robot operating system. In: ICRA workshop on open source software, vol\u00a03. IEEE Press, p\u00a05"},{"issue":"1","key":"328_CR22","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/2430536.2430537","volume":"22","author":"J Sun","year":"2013","unstructured":"Sun J, Liu Y, Dong JS, Liu Y, Shi L, Andr\u00e9 \u00c9 (2013) Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans Softw Eng Methodol 22(1):3","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"328_CR23","doi-asserted-by":"crossref","unstructured":"Sun J, Liu Y, Dong JS, Pang J (2009) PAT: towards flexible verification under fairness. In: CAV, vol\u00a09. Springer, Berlin, pp 709\u2013714","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"328_CR24","doi-asserted-by":"crossref","unstructured":"Wang M, Tian C, Duan Z (2017) Full regular temporal property verification as dynamic program execution. In: Proceedings of the 39th international conference on software engineering companion. IEEE Press, pp 226\u2013228","DOI":"10.1109\/ICSE-C.2017.98"},{"issue":"5","key":"328_CR25","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/s11704-016-6059-4","volume":"11","author":"X Wang","year":"2017","unstructured":"Wang X, Tian C, Duan Z, Zhao L (2017) MSVL: a typed language for temporal logic programming. Front Comput Sci 11(5):762\u2013785","journal-title":"Front Comput Sci"},{"issue":"1","key":"328_CR26","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L Waszniowski","year":"2008","unstructured":"Waszniowski L, Hanz\u00e1lek Z (2008) Formal verification of multitasking applications based on timed automata model. Real-Time Syst 38(1):39\u201365","journal-title":"Real-Time Syst"},{"key":"328_CR27","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/j.future.2015.05.008","volume":"56","author":"H Wei","year":"2016","unstructured":"Wei H, Shao Z, Huang Z, Chen R, Guan Y, Tan J, Shao Z (2016) RT-ROS: a real-time ROS architecture on multi-core processors. Future Gener Comput Syst 56:171\u2013178","journal-title":"Future Gener Comput Syst"},{"issue":"1","key":"328_CR28","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.jlap.2008.08.001","volume":"78","author":"X Yang","year":"2008","unstructured":"Yang X, Duan Z (2008) Operational semantics of framed tempura. J Logic Algebraic Program 78(1):22\u201351","journal-title":"J Logic Algebraic Program"},{"key":"328_CR29","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/j.tcs.2016.02.037","volume":"654","author":"N Zhang","year":"2016","unstructured":"Zhang N, Duan Z, Tian C (2016) A mechanism of function calls in MSVL. Theor Comput Sci 654:11\u201325","journal-title":"Theor Comput Sci"},{"issue":"11","key":"328_CR30","doi-asserted-by":"publisher","first-page":"118101","DOI":"10.1007\/s11432-015-0882-6","volume":"59","author":"N Zhang","year":"2016","unstructured":"Zhang N, Duan Z, Tian C (2016) Model checking concurrent systems with MSVL. Sci China Inf Sci 59(11):118101","journal-title":"Sci China Inf Sci"}],"container-title":["Journal of Combinatorial Optimization"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-018-0328-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10878-018-0328-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-018-0328-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,6]],"date-time":"2020-11-06T02:11:10Z","timestamp":1604628670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10878-018-0328-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,17]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["328"],"URL":"https:\/\/doi.org\/10.1007\/s10878-018-0328-0","relation":{},"ISSN":["1382-6905","1573-2886"],"issn-type":[{"type":"print","value":"1382-6905"},{"type":"electronic","value":"1573-2886"}],"subject":[],"published":{"date-parts":[[2018,7,17]]},"assertion":[{"value":"17 July 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}