{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:56:23Z","timestamp":1750308983540,"version":"3.41.0"},"reference-count":6,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,11,22]],"date-time":"2017-11-22T00:00:00Z","timestamp":1511308800000},"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":[[2017,11,22]]},"abstract":"<jats:p>\n            Several methods have been proposed for performing schedulability analysis for both uni-processor and multi-processor real-time systems. Very few of these works use the power of formal logic to write unambiguous specifications and to allow the usage of theorem provers for building the proofs of interest with greater correctness guarantees. In this paper we address this challenge by: 1) defining a formal language that allows to specify periodic resource models; 2) describe a transformational approach to reasoning about timing properties of resource models by transforming the latter specifications into a\n            <jats:italic>satisfiability modulo theories<\/jats:italic>\n            problem.\n          <\/jats:p>","DOI":"10.1145\/3166227.3166234","type":"journal-article","created":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T13:24:24Z","timestamp":1511789064000},"page":"40-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["SMT-based schedulability analysis using RMTL-\u222b"],"prefix":"10.1145","volume":"14","author":[{"given":"Andr\u00e9","family":"de Matos Pedro","sequence":"first","affiliation":[{"name":"CISTER\/INESC TEC, Porto, Portugal"}]},{"given":"David","family":"Pereira","sequence":"additional","affiliation":[{"name":"CISTER\/INESC TEC, Porto, Portugal"}]},{"given":"Lu\u00eds Miguel","family":"Pinho","sequence":"additional","affiliation":[{"name":"CISTER\/INESC TEC, Porto, Portugal"}]},{"given":"Jorge Sousa","family":"Pinto","sequence":"additional","affiliation":[{"name":"Universidade do Minho and Rua da Universidade, Braga, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2017,11,22]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Department of Computer Science","author":"Barrett Clark","year":"2015","unstructured":"Clark Barrett , Pascal Fontaine , and Cesare Tinelli . The SMT-LIB Standard: Version 2.5. Technical report , Department of Computer Science , The University of Iowa , 2015 . Available at www.SMT-LIB.org. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa, 2015. Available at www.SMT-LIB.org."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00151-8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2752801.2752808"},{"key":"e_1_2_1_5_1","volume-title":"rmtld3synth Synthesis Tool","author":"Pedro A. M.","year":"2016","unstructured":"A. M. Pedro , D. Pereira , L.M. Pinho , and J.S. Pinto . rmtld3synth Synthesis Tool , 2016 . Available at https:\/\/github.com\/cistergit\/rmtld3synth\/, version 0.1-alpha. A. M. Pedro, D. Pereira, L.M. Pinho, and J.S. Pinto. rmtld3synth Synthesis Tool, 2016. Available at https:\/\/github.com\/cistergit\/rmtld3synth\/, version 0.1-alpha."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347383"}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3166227.3166234","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3166227.3166234","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:06Z","timestamp":1750282866000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3166227.3166234"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,22]]},"references-count":6,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,11,22]]}},"alternative-id":["10.1145\/3166227.3166234"],"URL":"https:\/\/doi.org\/10.1145\/3166227.3166234","relation":{},"ISSN":["1551-3688"],"issn-type":[{"type":"electronic","value":"1551-3688"}],"subject":[],"published":{"date-parts":[[2017,11,22]]},"assertion":[{"value":"2017-11-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}