{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:23:02Z","timestamp":1762298582652},"reference-count":23,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"5","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2017]]},"DOI":"10.1587\/transinf.2016edp7374","type":"journal-article","created":{"date-parts":[[2017,4,30]],"date-time":"2017-04-30T22:14:35Z","timestamp":1493590475000},"page":"1055-1066","source":"Crossref","is-referenced-by-count":10,"title":["SMT-Based Scheduling for Overloaded Real-Time Systems"],"prefix":"10.1587","volume":"E100.D","author":[{"given":"Zhuo","family":"CHENG","sequence":"first","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haitao","family":"ZHANG","sequence":"additional","affiliation":[{"name":"School of Information Science and Engineering, Lanzhou University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yasuo","family":"TAN","sequence":"additional","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuto","family":"LIM","sequence":"additional","affiliation":[{"name":"School of Information Science, Japan Advanced Institute of Science and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"[1] Z. Cheng, H. Zhang, Y. Tan, and Y. Lim, \u201cScheduling overload for real-time systems using SMT solver,\u201d Proc. 17th IEEE\/ACIS Int. Conf. on Software Eng., Artificial Intell., Networking and Parallel\/Distributed Computing, Shanghai, China, pp.189-194, May30 -June 1, 2016.","DOI":"10.1109\/SNPD.2016.7515899"},{"key":"2","doi-asserted-by":"crossref","unstructured":"[2] F. Zhang and A. Burns, \u201cSchedulability analysis for real-time systems with EDF scheduling,\u201d IEEE Trans. Comput., vol.58, no.9, pp.1250-1258, April 2009.","DOI":"10.1109\/TC.2009.58"},{"key":"3","doi-asserted-by":"crossref","unstructured":"[3] S.K. Baruah, J. Haritsa, and N. Sharma, \u201cOn-line scheduling to maximize task completions,\u201d Proc. 15th IEEE Real-Time Syst. Symp., San Juan, Puerto Rico, pp.228-236, Dec. 1994.","DOI":"10.1109\/REAL.1994.342713"},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] A. Burns, \u201cScheduling hard real-time systems: a review,\u201d Software Eng. J., vol.6, no.3, pp.116-128, May 1991.","DOI":"10.1049\/sej.1991.0015"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] S.K. Baruah and J.R. Haritsa, \u201cScheduling for overload in real-time systems,\u201d IEEE Trans. Comput., vol.46, no.9, pp.1034-1039, Sept. 1997.","DOI":"10.1109\/12.620484"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] G.C. Buttazzo, G. Lipari, and L. Abeni, \u201cElastic task model for adaptive rate control,\u201d Proc. 19th IEEE Real-Time Syst. Symp., Madrid, Spain, pp.286-295, Dec. 1998.","DOI":"10.1109\/REAL.1998.739754"},{"key":"7","doi-asserted-by":"crossref","unstructured":"[7] A. Marchand and M. Chetto, \u201cDynamic scheduling of periodic skippable tasks in an overloaded real-time system,\u201d Proc. 6th IEEE\/ACS Int. Conf. on Comput. Syst. and Applicat., Doha, Qatar, pp.456-464, April 2008.","DOI":"10.1109\/AICCSA.2008.4493573"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] C. Tres, L.B. Becker, and E. Nett, \u201cReal-time tasks scheduling with value control to predict timing faults during overload,\u201d Proc. 10th IEEE Int. Symp. on Object and Component-Oriented Real-Time Distributed Computing, Santorini Island, Greece, pp.354-358, May 2007.","DOI":"10.1109\/ISORC.2007.52"},{"key":"9","unstructured":"[9] S.-I. Hwang, C.-M. Chen, and A.K. Agrawala, \u201cScheduling an overloaded real-time system,\u201d Proc. 15th IEEE Int. Phoenix Conf. on Comput. and Commun., Arizona, USA, pp.22-28, March 1996."},{"key":"10","doi-asserted-by":"crossref","unstructured":"[10] R.I. Davis and A. Burns, \u201cA survey of hard real-time scheduling for multiprocessor systems,\u201d ACM Comput. Surv., vol.43, no.5, pp.35:1-35:44, Oct. 2011.","DOI":"10.1145\/1978802.1978814"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] C.L. Liu and J.W. Layland, \u201cScheduling algorithms for multiprogramming in a hard-real-time environment,\u201d J. ACM, vol.20, no.1, pp.40-61, Jan. 1973.","DOI":"10.1145\/321738.321743"},{"key":"12","unstructured":"[12] C. Barrett, R. Sebastiani, R. Seshia, and C. Tinelli, \u201cSatisfiability modulo theories,\u201d in Handbook of Satisfiability, vol.185, IOS Press, 2009."},{"key":"13","doi-asserted-by":"crossref","unstructured":"[13] L.D. Moura and N. Bj\u00f8rner, \u201cSatisfiability Modulo Theories: An Appetizer,\u201d Formal Methods: Foundations and Applications, vol.5902, pp.23-26, 2009.","DOI":"10.1007\/978-3-642-10452-7_3"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] L. Moura and N. Bj\u00f8rner, \u201cZ3: an efficient SMT solver,\u201d Proc. 14th Int. Conf. on Tools and Algorithms for the Construction and Anal. of Syst., Budapest, Hungary, LNCS 4963, pp.337-340, Springer-Verlag, 2008.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15","doi-asserted-by":"crossref","unstructured":"[15] B. Dutertre, \u201cYices 2.2,\u201d Proc. 26th Int. Conf. on Comput. Aided Verification, Vienna, Austria, LNCS 8559, pp.737-744, Springer International Publishing, 2014.","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"16","doi-asserted-by":"crossref","unstructured":"[16] A. Metzner and C. Herde, \u201cRTSAT-An optimal and efficient approach to the task allocation problem in distributed architectures,\u201d Proc. RTSS, pp.147-158, 2006.","DOI":"10.1109\/RTSS.2006.44"},{"key":"17","doi-asserted-by":"crossref","unstructured":"[17] W. Liu, M. Yuan, X. He, Z. Gu, and X. Liu, \u201cEfficient SAT-based mapping and scheduling of homogeneous synchronous data flow graphs for throughput optimization,\u201d Proc. RTSS, pp.492-504, 2008.","DOI":"10.1109\/RTSS.2008.49"},{"key":"18","doi-asserted-by":"crossref","unstructured":"[18] W. Liu, Z. Gu, J. Xu, X. Wu, and Y. Ye, \u201cSatisfiability modulo graph theory for task mapping and scheduling on multiprocessor systems,\u201d IEEE Trans. Parallel Distribution Systems, vol.22, no.8, pp.1382-1389, 2011.","DOI":"10.1109\/TPDS.2010.204"},{"key":"19","doi-asserted-by":"crossref","unstructured":"[19] P. Kumar, D.B. Chokshi, and L. Thiele, \u201cA satisfiability approach to speed assignment for distributed real-time systems,\u201d Proc. DATE, pp.749-754, 2013.","DOI":"10.7873\/DATE.2013.160"},{"key":"20","unstructured":"[20] P. Tendulkar, P. Poplavko, and O. Maler, \u201cStrictly Periodic Scheduling of Acyclic Synchronous Dataflow Graphs using SMT Solvers,\u201d Verimag Research Report, pp.1-19, 2014."},{"key":"21","unstructured":"[21] P. Tendulkar, Mapping and Scheduling on Multi-core Processors using SMT Solvers, Ph.D. Thesis, 2014."},{"key":"22","doi-asserted-by":"crossref","unstructured":"[22] R. Bruttomesso, A. Cimatti, and et al., \u201cThe MathSAT 4 SMT Solver,\u201d Proc. CAV, pp.299-303, 2008.","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"23","doi-asserted-by":"crossref","unstructured":"[23] T. Ball, S.K. Lahiri, and M. Musuvathi, \u201cZap: Automated Theorem Proving for Software Analysis,\u201d Proc. LPAR, pp.2-22, 2005.","DOI":"10.1007\/11591191_2"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E100.D\/5\/E100.D_2016EDP7374\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T15:44:05Z","timestamp":1569167045000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E100.D\/5\/E100.D_2016EDP7374\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":23,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2016edp7374","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}