{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:16Z","timestamp":1762459276156,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192482"},{"type":"electronic","value":"9783319192499"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_34","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"551-569","source":"Crossref","is-referenced-by-count":7,"title":["Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking"],"prefix":"10.1007","author":[{"given":"Xue-Yang","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rongjie","family":"Yan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu-Lei","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenhui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guangquan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"34_CR1","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/j.tcs.2005.11.018","volume":"354","author":"Y. Abdedda\u00efm","year":"2006","unstructured":"Abdedda\u00efm, Y., Asarin, E., Maler, O., et al.: Scheduling with timed automata. Theor. Comput. Sci.\u00a0354(2), 272\u2013300 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"Ad\u00e9, M., Lauwereins, R., Peperstraete, J.: Data memory minimisation for synchronous data flow graphs emulated on DSP-FPGA targets. In: Proc. of the 34th Ann. Design Automation Conf (DAC), pp. 64\u201369 (1997)","DOI":"10.1145\/266021.266036"},{"issue":"2","key":"34_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11561163_8","volume-title":"Formal Methods for Components and Objects","author":"G. Behrmann","year":"2005","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Priced timed automata: Algorithms and applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol.\u00a03657, pp. 162\u2013182. Springer, Heidelberg (2005)"},{"issue":"9","key":"34_CR5","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1145\/1995376.1995396","volume":"54","author":"P. Bouyer","year":"2011","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Quantitative analysis of real-time systems using priced timed automata. Comm. of the ACM\u00a054(9), 78\u201387 (2011)","journal-title":"Comm. of the ACM"},{"issue":"4","key":"34_CR6","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer\u00a02(4), 410\u2013425 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"Fakih, M., Gr\u00fcttner, K., Fr\u00e4nzle, M., Rettberg, A.: Towards performance analysis of SDFGs mapped to shared-bus architectures using model-checking. In: Proc. of the Conference on Design, Automation and Test in Europe, pp. 1167\u20131172 (2013)","DOI":"10.7873\/DATE.2013.243"},{"issue":"2","key":"34_CR8","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/j.tcs.2005.11.019","volume":"354","author":"E. Fersman","year":"2006","unstructured":"Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci.\u00a0354(2), 301 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"34_CR9","doi-asserted-by":"crossref","unstructured":"Geilen, M., Basten, T., Stuijk, S.: Minimising buffer requirements of synchronous dataflow graphs with model checking. In: Proc. of the 42nd Annu. Design Automation Conf. (DAC) (2005)","DOI":"10.1145\/1065579.1065796"},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"Gu, Z., Yuan, M., Guan, N., Lv, M., He, X., Deng, Q., Yu, G.: Static scheduling and software synthesis for dataflow graphs with symbolic model-checking. In: Proc. of 28th International Real-Time Systems Symposium (RTSS), pp. 353\u2013364 (2007)","DOI":"10.1109\/RTSS.2007.51"},{"issue":"1","key":"34_CR11","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1109\/32.263752","volume":"20","author":"M.G. Harbour","year":"1994","unstructured":"Harbour, M.G., Klein, M.H., Lehoczky, J.P.: Timing analysis for fixed-priority scheduling of hard real-time systems. IEEE Trans. on Soft. Eng.\u00a020(1), 13\u201328 (1994)","journal-title":"IEEE Trans. on Soft. Eng."},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Hartel, P.H., Ruys, T.C., Geilen, M.C.: Scheduling optimisations for SPIN to minimise buffer requirements in synchronous data flow. In: Proc of the International Conference on Formal Methods in Computer-Aided Design, p. 21 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.25"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"Hirzel, M., Soul\u00e9, R., Schneider, S., Gedik, B., Grimm, R.: A catalog of stream processing optimizations. ACM Comput. Surv.\u00a046(4), 46:1\u201346:34 (2014)","DOI":"10.1145\/2528412"},{"issue":"5","key":"34_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"34_CR15","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer (STTT)\u00a01(1), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"1","key":"34_CR16","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/TC.1987.5009446","volume":"36","author":"E. Lee","year":"1987","unstructured":"Lee, E., Messerschmitt, D.: Static scheduling of synchronous data flow programs for digital signal processing. IEEE Trans. Comput.\u00a036(1), 24\u201335 (1987)","journal-title":"IEEE Trans. Comput."},{"key":"34_CR17","doi-asserted-by":"crossref","unstructured":"Madsen, J., Hansen, M.R., Knudsen, K.S., Nielsen, J.E., Brekling, A.W.: System-level verification of multi-core embedded systems using timed-automata. In: Proc. of the 17th World Congress International Federation of Automatic Control, Seoul, Korea, pp. 9302\u20139307 (2008)","DOI":"10.3182\/20080706-5-KR-1001.01572"},{"key":"34_CR18","doi-asserted-by":"crossref","unstructured":"Malik, A., Gregg, D.: Orchestrating stream graphs using model checking. ACM Trans. Archit. Code Optim.\u00a010(3), 19:1\u201319:25 (2013)","DOI":"10.1145\/2512435"},{"issue":"2","key":"34_CR19","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/12.73588","volume":"40","author":"K.K. Parhi","year":"1991","unstructured":"Parhi, K.K., Messerschmitt, D.G.: Static rate-optimal scheduling of iterative data-flow programs via optimum unfolding. IEEE Trans. Comput.\u00a040(2), 178\u2013195 (1991)","journal-title":"IEEE Trans. Comput."},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Singh, A.K., Shafique, M., Kumar, A., Henkel, J.: Mapping on multi\/many-core systems: Survey of current and emerging trends. In: Proc. of the 50th Ann. Design Automation Conf. (DAC), p. 1 (2013)","DOI":"10.1145\/2463209.2488734"},{"key":"34_CR21","unstructured":"Sriram, S., Bhattacharyya, S.S.: Embedded multiprocessors: scheduling and synchronization. CRC Press (2009)"},{"issue":"10","key":"34_CR22","doi-asserted-by":"publisher","first-page":"1331","DOI":"10.1109\/TC.2008.58","volume":"57","author":"S. Stuijk","year":"2008","unstructured":"Stuijk, S., Geilen, M., Basten, T.: Throughput-buffering trade-off exploration for cyclo-static and synchronous dataflow graphs. IEEE Trans. Comput.\u00a057(10), 1331\u20131345 (2008)","journal-title":"IEEE Trans. Comput."},{"key":"34_CR23","doi-asserted-by":"crossref","unstructured":"Theelen, B., Katoen, J.P., Wu, H.: Model checking of scenario-aware dataflow with CADP. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 653\u2013658 (2012)","DOI":"10.1109\/DATE.2012.6176552"},{"key":"34_CR24","doi-asserted-by":"crossref","unstructured":"Zhu, X.-Y., Geilen, M., Basten, T., Stuijk, S.: Static rate-optimal scheduling of multirate DSP algorithms via retiming and unfolding. In: Proc. of the 18th Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 109\u2013118 (2012)","DOI":"10.1109\/RTAS.2012.15"},{"key":"34_CR25","unstructured":"Zivojnovic, V., Ritz, S., Meyr, H.: Optimizing DSP programs using the multirate retiming transformation. Proc. EUSIPCO Signal Process. VII, Theories Applicat. (1994)"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T12:23:59Z","timestamp":1675859039000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}