{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:25Z","timestamp":1750306585212,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,3,27]],"date-time":"2015-03-27T00:00:00Z","timestamp":1427414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGBED Rev."],"published-print":{"date-parts":[[2015,3,27]]},"abstract":"<jats:p>Over the past decades several approaches for schedulability analysis have been proposed for both uni-processor and multi-processor real-time systems. Although different techniques are employed, very little has been put forward in using formal specifications, with the consequent possibility for misinterpretations or ambiguities in the problem statement. Using a logic based approach to schedulability analysis in the design of hard real-time systems eases the synthesis of correct-by-construction procedures for both static and dynamic verification processes. In this paper we propose a novel approach to schedulability analysis based on a timed temporal logic with time durations. Our approach subsumes classical methods for uni-processor scheduling analysis over compositional resource models by providing the developer with counter-examples, and by ruling out schedules that cause unsafe violations on the system. We also provide an example showing the effectiveness of our proposal.<\/jats:p>","DOI":"10.1145\/2752801.2752808","type":"journal-article","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T14:59:12Z","timestamp":1427900352000},"page":"56-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Logic-based schedulability analysis for compositional hard real-time embedded systems"],"prefix":"10.1145","volume":"12","author":[{"given":"Andr\u00e9","family":"de Matos Pedro","sequence":"first","affiliation":[{"name":"CISTER\/INESC TEC, ISEP, Porto, Portugal"}]},{"given":"David","family":"Pereira","sequence":"additional","affiliation":[{"name":"CISTER\/INESC TEC, ISEP, Porto, Portugal"}]},{"given":"Lu\u00eds Miguel","family":"Pinho","sequence":"additional","affiliation":[{"name":"CISTER\/INESC TEC, ISEP, Porto, Portugal"}]},{"given":"Jorge Sousa","family":"Pinto","sequence":"additional","affiliation":[{"name":"HASLab\/INESC TEC, UM, Rua da Universidade, Braga, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2015,3,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01094342"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008047130023"},{"key":"e_1_2_1_4_1","first-page":"53","volume-title":"Boogie 2011: First International Workshop on Intermediate Verification Languages","author":"Bobot F.","year":"2011","unstructured":"F. Bobot , J. C. Filli &ccirc;tre, C. March\u00e9 , and A. Paskevich . Why3: Shepherd Your Herd of Provers . In Boogie 2011: First International Workshop on Intermediate Verification Languages , pages 53 -- 64 , 2011 . F. Bobot, J. C. Filli&ccirc;tre, C. March\u00e9, and A. Paskevich. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 53--64, 2011."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0021-4"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"e_1_2_1_7_1","volume-title":"Model checking","author":"Clarke E. M.","year":"1999","unstructured":"E. M. Clarke , O. Grumberg , and D. A. Peled . Model checking . MIT Press , Cambridge, MA, USA , 1999 . E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, Cambridge, MA, USA, 1999."},{"key":"e_1_2_1_8_1","volume-title":"Boogiepl: A typed procedural language for checking object-oriented programs. Technical report","author":"Deline Robert","year":"2005","unstructured":"Robert Deline , K. Rustan , and M. Leino . Boogiepl: A typed procedural language for checking object-oriented programs. Technical report , 2005 . Robert Deline, K. Rustan, and M. Leino. Boogiepl: A typed procedural language for checking object-oriented programs. Technical report, 2005."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.01.009"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.019"},{"key":"e_1_2_1_11_1","first-page":"67","volume-title":"Timed Automata with Asynchronous Processes: Schedulability and Decidability. TACAS '02","author":"Fersman E.","year":"2002","unstructured":"E. Fersman , P. Pettersson , and W. Yi . Timed Automata with Asynchronous Processes: Schedulability and Decidability. TACAS '02 , pages 67 -- 82 , 2002 . E. Fersman, P. Pettersson, and W. Yi. Timed Automata with Asynchronous Processes: Schedulability and Decidability. TACAS '02, pages 67--82, 2002."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007993819750"},{"key":"e_1_2_1_13_1","first-page":"31","volume-title":"DIPES '02","author":"Gu Z.","year":"2002","unstructured":"Z. Gu and K. G. Shin . Analysis of event-driven real-time systems with time petri nets: A translation-based approach . DIPES '02 , pages 31 -- 40 , 2002 . Z. Gu and K. G. Shin. Analysis of event-driven real-time systems with time petri nets: A translation-based approach. DIPES '02, pages 31--40, 2002."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779879.1779899"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"P.\n      Kr\u010d\u00e1l\n     and \n      W.\n      Yi\n  . \n  Decidable and undecidable problems in schedulability analysis using timed automata\n  . volume \n  2988\n   of \n  TACAS'04 pages \n  236\n  --\n  250\n  . \n  Springer-Verlag 2004\n  .  P. Kr\u010d\u00e1l and W. Yi. Decidable and undecidable problems in schedulability analysis using timed automata. volume 2988 of TACAS'04 pages 236--250. Springer-Verlag 2004.","DOI":"10.1007\/978-3-540-24730-2_20"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00151-8"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1989.63567"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/321738.321743"},{"key":"e_1_2_1_19_1","volume-title":"FoVeOOS'10","author":"Pariente Dillon","year":"2010","unstructured":"Dillon Pariente and Emmanuel Ledinot . Formal Verification of Industrial C Code using Frama-C: a Case Study . FoVeOOS'10 , 2010 . Dillon Pariente and Emmanuel Ledinot. Formal Verification of Industrial C Code using Frama-C: a Case Study. FoVeOOS'10, 2010."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1885174.1885189"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939399.1939428"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35632-2_23"},{"key":"e_1_2_1_23_1","first-page":"2","volume-title":"Periodic Resource Model for Compositional Real-Time Guarantees. RTSS '03","author":"Shin I.","year":"2003","unstructured":"I. Shin and I. Lee . Periodic Resource Model for Compositional Real-Time Guarantees. RTSS '03 , pages 2 -- 13 , 2003 . I. Shin and I. Lee. Periodic Resource Model for Compositional Real-Time Guarantees. RTSS '03, pages 2--13, 2003."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347383"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.341845"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2009.23"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2010.18"}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2752801.2752808","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2752801.2752808","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:22Z","timestamp":1750227382000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2752801.2752808"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,27]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3,27]]}},"alternative-id":["10.1145\/2752801.2752808"],"URL":"https:\/\/doi.org\/10.1145\/2752801.2752808","relation":{},"ISSN":["1551-3688"],"issn-type":[{"type":"electronic","value":"1551-3688"}],"subject":[],"published":{"date-parts":[[2015,3,27]]},"assertion":[{"value":"2015-03-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}