{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T23:40:05Z","timestamp":1749598805973,"version":"3.41.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471655"},{"type":"electronic","value":"9783319471662"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47166-2_7","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T22:07:34Z","timestamp":1475618854000},"page":"94-113","source":"Crossref","is-referenced-by-count":5,"title":["Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego"],"prefix":"10.1007","author":[{"given":"Waheed","family":"Ahmad","sequence":"first","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Ahmad, W., de Groote, R., H\u00f6lzenspies, P.K.F., Stoelinga, M., van de Pol, J.: Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata. In: Proceedings of 14th International Conference on Application of Concurrency to System Design, (ACSD), pp. 72\u201381 (2014)","DOI":"10.1109\/ACSD.2014.13"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Ahmad, W., H\u00f6lzenspies, P.K.F., Stoelinga, M., van de Pol, J.: Green computing: power optimisation of VFI-based real-time multiprocessor dataflow applications. In: Proceedings of 18th Euromicro Conference on Digital Systems Design (DSD), pp. 271\u2013275 (2015)","DOI":"10.1109\/DSD.2015.59"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Ahmad, W., Jongerden, M., Stoelinga, M., van de Pol, J.: Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata. In: Proceedings of 16th International Conference on Application of Concurrency to System Design (ACSD), pp. 114\u2013123 (2016)","DOI":"10.1109\/ACSD.2016.18"},{"key":"7_CR4","unstructured":"Ahmad, W., Yildiz, B.M., Rensink, A., Stoelinga, M.: Evaluating the tools on the face detection and recognition case study, Chap. 2, pp. 4\u20136. FP7 EU Project SENSATION, Deliverable D1.4 (2016)"},{"key":"7_CR5","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"issue":"4","key":"7_CR7","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1145\/1059816.1059823","volume":"32","author":"G Behrmann","year":"2005","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. SIGMETRICS Perform. Eval. Rev. 32(4), 34\u201340 (2005)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"issue":"3","key":"7_CR8","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1109\/92.845896","volume":"8","author":"L Benini","year":"2000","unstructured":"Benini, L., Bogliolo, A., Micheli, G.D.: A survey of design techniques for system-level dynamic power management. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 8(3), 299\u2013316 (2000)","journal-title":"IEEE Trans. Very Large Scale Integr. (VLSI) Syst."},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66\u201380. Springer, Heidelberg (2005). doi: 10.1007\/11539452_9"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"David, A., Du, D., Larsen, K.G., Legay, A., Miku\u010dionis, M., B\u00f8gsted Poulsen, D., Sedwards, S.: Statistical model checking for stochastic hybrid systems. ArXiv e-prints (2012)","DOI":"10.4204\/EPTCS.92.9"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-11936-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"A David","year":"2014","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., S\u00f8rensen, M.G., Taankvist, J.H.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129\u2013145. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-11936-6_10"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Miku\u010dionis, M., Taankvist, J.H.: Uppaal\u00a0Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_16"},{"issue":"4","key":"7_CR13","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"7_CR14","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1109\/TC.2010.248","volume":"61","author":"V Devadas","year":"2012","unstructured":"Devadas, V., Aydin, H.: On the interplay of voltage\/frequency scaling and device power management for frame-based real-time embedded applications. IEEE Trans. Comput. 61(1), 31\u201344 (2012)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR15","first-page":"1742","volume":"64","author":"MET Gerards","year":"2014","unstructured":"Gerards, M.E.T., Hurink, J.L., Kuper, J.: On the interplay between global DVFS and scheduling tasks with precedence constraints. IEEE Trans. Comput. 64, 1742\u20131754 (2014)","journal-title":"IEEE Trans. Comput."},{"issue":"12","key":"7_CR16","doi-asserted-by":"crossref","first-page":"1682","DOI":"10.1109\/TC.2012.136","volume":"61","author":"JJ Han","year":"2012","unstructured":"Han, J.J., Wu, X., Zhu, D., Jin, H., Yang, L.T., Gaudiot, J.L.: Synchronization-aware energy management for VFI-based multicore real-time systems. IEEE Trans. Comput. 61(12), 1682\u20131696 (2012)","journal-title":"IEEE Trans. Comput."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Proceedings of Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 278\u2013292 (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Herbert, S., Marculescu, D.: Analysis of dynamic voltage\/frequency scaling in chip-multiprocessors. In: Proceedings of ACM\/IEEE International Symposium on Low Power Electronics and Design (ISLPED), pp. 38\u201343 (2007)","DOI":"10.1145\/1283780.1283790"},{"issue":"2","key":"7_CR19","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/1067309.1067324","volume":"36","author":"S Irani","year":"2005","unstructured":"Irani, S., Pruhs, K.R.: Algorithmic problems in power management. ACM SIGACT News 36(2), 63\u201376 (2005)","journal-title":"ACM SIGACT News"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Wu, H., Exponentially timed SADF: compositional semantics, reductions, and analysis. In: Proceedings of 14th ACM\/IEEE International Conference on Embedded Software (EMSOFT), pp. 1:1\u20131:10 (2014)","DOI":"10.1145\/2656045.2656058"},{"issue":"9","key":"7_CR21","doi-asserted-by":"crossref","first-page":"1235","DOI":"10.1109\/PROC.1987.13876","volume":"75","author":"EA Lee","year":"1987","unstructured":"Lee, E.A., Messerschmitt, D.G.: Synchronous data flow. Proc. IEEE 75(9), 1235\u20131245 (1987)","journal-title":"Proc. IEEE"},{"issue":"5","key":"7_CR22","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1016\/0038-092X(93)90060-2","volume":"50","author":"JF Manwell","year":"1993","unstructured":"Manwell, J.F., McGowan, J.G.: Lead acid battery storage model for hybrid energy systems. Sol. Energy 50(5), 399\u2013405 (1993)","journal-title":"Sol. Energy"},{"issue":"8","key":"7_CR23","doi-asserted-by":"crossref","first-page":"1282","DOI":"10.1093\/comjnl\/bxr008","volume":"54","author":"JL March","year":"2011","unstructured":"March, J.L., Sahuquillo, J., Hassan, H., Petit, S., Duato, J.: A new energy-aware dynamic task set partitioning algorithm for soft and hard embedded real-time systems. Comput. J. 54(8), 1282\u20131294 (2011)","journal-title":"Comput. J."},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Nelson, A., Moreira, O., Molnos, A., Stuijk, S., Nguyen, B.T., Goossens, K.: Power minimisation for real-time dataflow applications. In: Proceedings of 14th Euromicro Conference on Digital System Design (DSD), pp. 117\u2013124 (2011)","DOI":"10.1109\/DSD.2011.19"},{"issue":"5","key":"7_CR25","doi-asserted-by":"crossref","first-page":"695","DOI":"10.1109\/TCAD.2012.2235126","volume":"32","author":"S Park","year":"2013","unstructured":"Park, S., Park, J., Shin, D., Wang, Y., Xie, Q., Pedram, M., Chang, N.: Accurate modeling of the delay and energy overhead of dynamic voltage and frequency scaling in modern microprocessors. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 32(5), 695\u2013708 (2013)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."},{"key":"7_CR26","unstructured":"ter Braak, T.D., Sunesen, K., Ahmad, W., Stoelinga, M., van de Pol, J., Katoen, J.-P., Wu, H.: Evaluating the tools on the face detection and recognition case study, Chap. 2, pp. 6\u201323. FP7 EU Project SENSATION, Deliverable D4.4 (2016)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Theelen, B., Geilen, M., Basten, T., Voeten, J., Gheorghita, S., Stuijk, S.: A scenario-aware data flow model for combined long-run average and worst-case performance analysis. In: Proceedings of 4th ACM\/IEEE International Conference on Formal Methods and Models for Co-design (MEMOCODE), pp. 185\u2013194 (2006)","DOI":"10.1109\/MEMCOD.2006.1695924"},{"key":"7_CR28","unstructured":"Weiser, M., Welch, B., Demers, A., Shenker, S.: Scheduling for reduced CPU energy. In: Proceedings of 1st USENIX Conference on Operating Systems Design and Implementation (1994)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-22975-1_20","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"ER Wognsen","year":"2015","unstructured":"Wognsen, E.R., Haverkort, B.R., Jongerden, M., Hansen, R.R., Larsen, K.G.: A score function for optimizing the cycle-life of battery-powered embedded systems. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 305\u2013320. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-22975-1_20"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Yang, Y., Geilen, M., Basten, T., Stuijk, S., Corporaal, H.: Playing games with scenario- and resource-aware SDF graphs through policy iteration. In: Proceedings of Design, Automation and Test in Europe (DATE), pp. 194\u2013199 (2012)","DOI":"10.1109\/DATE.2012.6176462"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Zhu, J., Sander, I., Jantsch, A.: Energy efficient streaming applications with guaranteed throughput on MPSoCs. In: Proceedings of 8th ACM\/IEEE International Conference on Embedded Software (EMSOFT), pp. 119\u2013128 (2008)","DOI":"10.1145\/1450058.1450075"},{"issue":"7","key":"7_CR32","doi-asserted-by":"crossref","first-page":"1447","DOI":"10.1109\/TPDS.2012.20","volume":"24","author":"S Zhuravlev","year":"2013","unstructured":"Zhuravlev, S., Saez, J.C., Blagodurov, S., Fedorova, A., Prieto, M.: Survey of energy-cognizant scheduling techniques. IEEE Trans. Parallel Distrib. Syst. 24(7), 1447\u20131464 (2013)","journal-title":"IEEE Trans. Parallel Distrib. Syst."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T23:09:23Z","timestamp":1749596963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}