{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T00:14:02Z","timestamp":1767140042706,"version":"build-2238731810"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,2]]},"DOI":"10.1007\/s10009-019-00521-7","type":"journal-article","created":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T13:29:31Z","timestamp":1559395771000},"page":"3-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Correct-by-construction model-based design of reactive streaming software for multi-core embedded systems"],"prefix":"10.1007","volume":"22","author":[{"given":"Fotios","family":"Gioulekas","sequence":"first","affiliation":[]},{"given":"Peter","family":"Poplavko","sequence":"additional","affiliation":[]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Pedro","family":"Palomo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,6,1]]},"reference":[{"key":"521_CR1","doi-asserted-by":"publisher","unstructured":"Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: Proceedings of the Tenth ACM International Conference on Embedded Software, EMSOFT \u201910. ACM, New York, NY, USA, pp. 229\u2013238 (2010). \nhttps:\/\/doi.org\/10.1145\/1879021.1879052","DOI":"10.1145\/1879021.1879052"},{"key":"521_CR2","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-540-40903-8_6","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T Amnell","year":"2004","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Times: a tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.G., Niebert, P. (eds.) Formal Modeling and Analysis of Timed Systems, pp. 60\u201372. Springer, Berlin (2004)"},{"key":"521_CR3","unstructured":"Autofocus tool. \nhttps:\/\/af3.fortiss.org\/\n\n. [Available Online; accessed: 05-February-2019]"},{"key":"521_CR4","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)"},{"key":"521_CR5","doi-asserted-by":"crossref","unstructured":"Basu, A., Bensalem, S., Bozga, M., Bourgos, P., Maheshwari, M., Sifakis, J.: Component assemblies in the context of manycore. In: Beckert, B., Damiani, F., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects: 10th International Symposium, FMCO 2011, Turin, Italy, October 3\u20135, 2011, Revised Selected Papers. Springer, Berlin, pp. 314\u2013333 (2013)","DOI":"10.1007\/978-3-642-35887-6_17"},{"key":"521_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2017.12.007","volume":"156","author":"G Brau","year":"2018","unstructured":"Brau, G., Hugues, J., Navet, N.: Towards the systematic analysis of non-functional properties in model-based engineering for real-time embedded systems. Sci. Comput. Program. 156, 1\u201320 (2018). \nhttps:\/\/doi.org\/10.1016\/j.scico.2017.12.007","journal-title":"Sci. Comput. Program."},{"key":"521_CR7","unstructured":"Broy, M., Dederichs, F., Dendorfer, C., Fuchs, M., Gritzner, T., Weber, R.: The design of distributed systems\u2014an introduction to focus. Tech. Rep. TUM-I 9202-2, Technische Universitat Munchen (1992)"},{"key":"521_CR8","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-1-4613-0091-5","volume-title":"Systems: Focus on Streams, Interfaces, and Refinement","author":"M Broy","year":"2001","unstructured":"Broy, M., Stolen, K.: Systems: Focus on Streams, Interfaces, and Refinement, p. 348. Springer, New York (2001). \nhttps:\/\/doi.org\/10.1007\/978-1-4613-0091-5"},{"key":"521_CR9","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-85289-6_8","volume-title":"Service-Oriented Modeling of CoCoME with Focus and AutoFocus","author":"M Broy","year":"2008","unstructured":"Broy, M., Fox, J., H\u00f6lzl, F., Koss, D., Kuhrmann, M., Meisinger, M., Penzenstadler, B., Rittmann, S., Sch\u00e4tz, B., Spichkova, M., Wild, D.: Service-Oriented Modeling of CoCoME with Focus and AutoFocus, pp. 177\u2013206. Springer, Berlin (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-85289-6_8"},{"key":"521_CR10","unstructured":"Chaki, S., Kyle, D.: DMPL: Programming and verifying distributed mixed-synchrony and mixed-critical software. Tech. rep., Carnegie Mellon University (2016). \nhttp:\/\/www.andrew.cmu.edu\/user\/schaki\/misc\/dmpl-extended.pdf"},{"key":"521_CR11","unstructured":"Claraz, D., Grimal, F., Laydier, T., Mader, R., Wirrer, G.: Introducing multi-core at automotive engine systems. In: ERTSS\u201914, Embedded Real-Time Software and Systems (2014)"},{"key":"521_CR12","unstructured":"Cordovilla, M., Boniol, F., Forget, J., Noulard, E., Pagetti, C.: Developing critical embedded systems on multicore architectures: the Prelude-SchedMCore toolset. In: RTNS (2011)"},{"issue":"1","key":"521_CR13","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1109\/JPROC.2002.805829","volume":"91","author":"J Eker","year":"2003","unstructured":"Eker, J., Janneck, J.W., Lee, E.A., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity\u2014the Ptolemy approach. Proc. IEEE 91(1), 127\u2013144 (2003)","journal-title":"Proc. IEEE"},{"key":"521_CR14","unstructured":"Feiler, P., Gluch, D., Hudak, J.: The architecture analysis & design language (AADL): an introduction. Tech. Rep. CMU\/SEI-2006-TN-011, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA (2006). \nhttp:\/\/resources.sei.cmu.edu\/library\/asset-view.cfm?AssetID=7879"},{"key":"521_CR15","doi-asserted-by":"crossref","unstructured":"Forget, J., Boniol, F., Grolleau, E., Lesens, D., Pagetti, C.: Scheduling dependent periodic tasks without synchronization mechanisms. In: RTAS\u201910, pp. 301\u2013310 (2010)","DOI":"10.1109\/RTAS.2010.26"},{"key":"521_CR16","doi-asserted-by":"publisher","unstructured":"Fuhrmann, H., von Hanxleden, R., Rennhack, J., Koch, J.: Model-based system design of time-triggered architectures\u2013 -avionics case study. In: 2006 IEEE\/AIAA 25th Digital Avionics Systems Conference, pp. 1\u201312 (2006). \nhttps:\/\/doi.org\/10.1109\/DASC.2006.313745","DOI":"10.1109\/DASC.2006.313745"},{"key":"521_CR17","doi-asserted-by":"crossref","unstructured":"Geilen, M., Basten, T.: Reactive process networks. In: EMSOFT\u201904. ACM, pp. 137\u2013146 (2004)","DOI":"10.1145\/1017753.1017778"},{"key":"521_CR18","doi-asserted-by":"crossref","unstructured":"Ghamarian, A.H.: Timing analysis of synchronous dataflow graphs. Ph.D. thesis, Eindhoven University of Technology (2008)","DOI":"10.1109\/DATE.2008.4484672"},{"issue":"1","key":"521_CR19","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10617-018-9206-3","volume":"22","author":"G Giannopoulou","year":"2018","unstructured":"Giannopoulou, G., Poplavko, P., Socci, D., Huang, P., Stoimenov, N., Bourgos, P., Thiele, L., Bozga, M., Bensalem, S., Girbal, S., Faugere, M., Soulat, R., de Dinechin, B.D.: DOL-BIP-critical: a tool chain for rigorous design and implementation of mixed-criticality multi-core systems. Des. Autom. Embed. Syst. 22(1), 141\u2013181 (2018). \nhttps:\/\/doi.org\/10.1007\/s10617-018-9206-3","journal-title":"Des. Autom. Embed. Syst."},{"key":"521_CR20","doi-asserted-by":"publisher","unstructured":"Gioulekas, F., Poplavko, P., Katsaros, P., Palomo, P.: Process network models for embedded system design based on the real-time bip execution engine. In: S.\u00a0Bliudze, S.\u00a0Bensalem (eds.) Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design, Thessaloniki, Greece, 15th April 2018, Electronic Proceedings in Theoretical Computer Science, vol. 272. Open Publishing Association, pp. 79\u201392 (2018). \nhttps:\/\/doi.org\/10.4204\/EPTCS.272.7","DOI":"10.4204\/EPTCS.272.7"},{"key":"521_CR21","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-319-89363-1_6","volume-title":"Fundamental Approaches to Software Engineering","author":"F Gioulekas","year":"2018","unstructured":"Gioulekas, F., Poplavko, P., Katsaros, P., Bensalem, S., Palomo, P.: A process network model for reactive streaming software with deterministic task parallelism. In: Russo, A., Sch\u00fcrr, A. (eds.) Fundamental Approaches to Software Engineering, pp. 94\u2013110. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89363-1_6"},{"key":"521_CR22","unstructured":"GR-CPCI-LEON4-N2X: Quad-core LEON4 next generation microprocessor evaluation board, \nhttp:\/\/www.gaisler.com\/index.php\/products\/boards\/gr-cpci-leon4-n2x"},{"issue":"3","key":"521_CR23","first-page":"24:1","volume":"12","author":"S Ha","year":"2008","unstructured":"Ha, S., Kim, S., Lee, C., Yi, Y., Kwon, S., Joo, Y.P.: PeaCE: a hardware-software codesign environment for multimedia embedded systems. ACM Trans. Des. Autom. Electron. Syst. 12(3), 24:1\u201324:25 (2008)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"521_CR24","volume-title":"Synchronous Programming of Reactive Systems","author":"N Halbwachs","year":"2010","unstructured":"Halbwachs, N.: Synchronous Programming of Reactive Systems. Springer, Berlin (2010)"},{"issue":"1","key":"521_CR25","first-page":"2","volume":"14","author":"A Hansson","year":"2009","unstructured":"Hansson, A., Goossens, K., Bekooij, M., Huisken, J.: CoMPSoC: a template for composable and predictable multi-processor system on chips. ACM Trans. Des. Autom. Electron. Syst. (TODAES) 14(1), 2 (2009)","journal-title":"ACM Trans. Des. Autom. Electron. Syst. (TODAES)"},{"key":"521_CR26","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-16277-0_13","volume-title":"13 AutoFocus 3\u2013A Scientific Tool Prototype for Model-Based Development of Component-Based, Reactive, Distributed Systems","author":"F H\u00f6lzl","year":"2010","unstructured":"H\u00f6lzl, F., Feilkas, M.: 13 AutoFocus 3\u2013A Scientific Tool Prototype for Model-Based Development of Component-Based, Reactive, Distributed Systems, pp. 317\u2013322. Springer, Berlin (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-16277-0_13"},{"key":"521_CR27","unstructured":"Huber, F., Molterer, S., Rausch, A., Schatz, B., Sihling, M., Slotosch, O.: Tool supported specification and simulation of distributed systems. In: B. Kramer, N. Uchihira, P. Croll, and S. Russo (eds.) International Symposium on Software Engineering for Parallel and Distributed Systems. IEEE, pp. 155\u2013164 (1998)"},{"issue":"4","key":"521_CR28","doi-asserted-by":"crossref","first-page":"42:1","DOI":"10.1145\/1376804.1376810","volume":"7","author":"J Hugues","year":"2008","unstructured":"Hugues, J., Zalila, B., Pautet, L., Kordon, F.: From the prototype to the final embedded system using the Ocarina AADL tool suite. ACM Trans. Embed. Comput. Syst. 7(4), 42:1\u201342:25 (2008)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"issue":"1","key":"521_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1013208.1013209","volume":"36","author":"WM Johnston","year":"2004","unstructured":"Johnston, W.M., Hanna, J.R.P., Millar, R.J.: Advances in dataflow programming languages. ACM Comput. Surv. 36(1), 1\u201334 (2004)","journal-title":"ACM Comput. Surv."},{"key":"521_CR30","unstructured":"Kahn, G.: The semantics of a simple language for parallel programming. In: J.L. Rosenfeld (ed.) Information Processing \u201974: Proceedings of the IFIP Congress. North-Holland, New York, NY, pp. 471\u2013475 (1974)"},{"issue":"1","key":"521_CR31","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/TC.1987.5009446","volume":"C\u201336","author":"EA Lee","year":"1987","unstructured":"Lee, E.A., Messerschmitt, D.G.: Static scheduling of synchronous data flow programs for digital signal processing. IEEE Trans. Comput. C\u201336(1), 24\u201335 (1987)","journal-title":"IEEE Trans. Comput."},{"issue":"9","key":"521_CR32","doi-asserted-by":"publisher","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). \nhttps:\/\/doi.org\/10.1109\/PROC.1987.13876","journal-title":"Proc. IEEE"},{"key":"521_CR33","doi-asserted-by":"publisher","unstructured":"Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M.: From AADL model to LNT specification. In: Reliable Software Technologies\u2014Ada-Europe 2015. Springer, Cham, pp. 11\u201320 (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19584-1_10","DOI":"10.1007\/978-3-319-19584-1_10"},{"key":"521_CR34","doi-asserted-by":"crossref","unstructured":"Perrotin, M., Conquet, E., Delange, J., Schiele, A., Tsiodras, T.: TASTE: a real-time software engineering tool-chain overview, status, and future. In: I.\u00a0Ober, I.\u00a0Ober (eds.) SDL 2011: Integrating System and Software Modeling. International SDL Forum. Revised Papers. Springer, Berlin, pp. 26\u201337 (2012)","DOI":"10.1007\/978-3-642-25264-8_4"},{"key":"521_CR35","doi-asserted-by":"publisher","unstructured":"Poplavko, P., Kahil, R., Socci, D., Bensalem, S., Bozga, M.: Mixed-critical systems design with coarse-grained multi-core interference. In: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, ISoLA\u201916. Springer, pp. 605\u2013621 (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-47166-2_42","DOI":"10.1007\/978-3-319-47166-2_42"},{"key":"521_CR36","doi-asserted-by":"publisher","unstructured":"Poplavko, P., Nouri, A., Angelis, L., Zerzelidis, A., Bensalem, S., Katsaros, P.: Regression-based statistical bounds on software execution time. In: Verification and Evaluation of Computer and Communication Systems\u201411th International Conference, VECoS 2017, Montreal, QC, Canada, August 24\u201325, 2017, Proceedings, pp. 48\u201363 (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66176-6_4","DOI":"10.1007\/978-3-319-66176-6_4"},{"key":"521_CR37","unstructured":"Poplavko, P., Socci, D., Bourgos, P., Bensalem, S., Bozga, M.: Models for deterministic execution of real-time multiprocessor applications. In: Proceedings of the 2015 Design, Automation and Test in Europe Conference and Exhibition, DATE \u201915. EDA Consortium, San Jose, CA, USA, pp. 1665\u20131670 (2015). \nhttp:\/\/dl.acm.org\/citation.cfm?id=2757012.2757198"},{"key":"521_CR38","doi-asserted-by":"publisher","unstructured":"Saidi, S.: On the benefits of multicores for real-time systems. In: 2017 Euromicro Conference on Digital System Design (DSD), pp. 383\u2013389 (2017). \nhttps:\/\/doi.org\/10.1109\/DSD.2017.85","DOI":"10.1109\/DSD.2017.85"},{"key":"521_CR39","doi-asserted-by":"publisher","unstructured":"Socci, D., Poplavko, P., Bensalem, S., Bozga, M.: A timed-automata based middleware for time-critical multicore applications. In: 2015 IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing Workshops, pp. 1\u20138 (2015). \nhttps:\/\/doi.org\/10.1109\/ISORCW.2015.55","DOI":"10.1109\/ISORCW.2015.55"},{"key":"521_CR40","unstructured":"Time-critical applications on multicore platforms. \nhttp:\/\/www-verimag.imag.fr\/Time-Critical-Applications-on-Multicore.html"},{"key":"521_CR41","doi-asserted-by":"crossref","unstructured":"Triki, A., Combaz, J., Bensalem, S., Sifakis, J.: Model-based implementation of parallel real-time systems. In: Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering, FASE\u201913. Springer, Berlin, pp. 235\u2013249 (2013)","DOI":"10.1007\/978-3-642-37057-1_18"},{"key":"521_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.cosrev.2013.05.001","volume":"9","author":"MTB Waez","year":"2013","unstructured":"Waez, M.T.B., Dingel, J., Rudie, K.: A survey of timed automata for the development of real-time systems. Comput. Sci. Rev. 9, 1\u201326 (2013)","journal-title":"Comput. Sci. Rev."},{"key":"521_CR43","doi-asserted-by":"publisher","unstructured":"Yang, Z., Hu, K., Ma, D., Pi, L.: Towards a formal semantics for the AADL behavior annex. In: 2009 Design, Automation Test in Europe Conference Exhibition, pp. 1166\u20131171 (2009). \nhttps:\/\/doi.org\/10.1109\/DATE.2009.5090839","DOI":"10.1109\/DATE.2009.5090839"},{"key":"521_CR44","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.jss.2014.02.058","volume":"93","author":"Z Yang","year":"2014","unstructured":"Yang, Z., Hu, K., Ma, D., Bodeveix, J.P., Pi, L., Talpin, J.P.: From aadl to timed abstract state machines: a verified model transformation. J. Syst. Softw. 93, 42\u201368 (2014). \nhttps:\/\/doi.org\/10.1016\/j.jss.2014.02.058","journal-title":"J. Syst. Softw."}],"updated-by":[{"DOI":"10.1007\/s10009-019-00523-5","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T00:00:00Z","timestamp":1562889600000}}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00521-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00521-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00521-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,30]],"date-time":"2020-05-30T19:09:57Z","timestamp":1590865797000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00521-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,1]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,2]]}},"alternative-id":["521"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00521-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,6,1]]},"assertion":[{"value":"1 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2019","order":2,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Updated Fig. 7 (<Emphasis Type=\"Italic\">p<\/Emphasis><Subscript><Emphasis Type=\"Italic\">i<\/Emphasis><\/Subscript> is the job\u2019s process,<Emphasis Type=\"Italic\"> k<\/Emphasis><Subscript><Emphasis Type=\"Italic\">i<\/Emphasis><\/Subscript> is the job\u2019s invocation count,<Emphasis Type=\"Italic\"> A<\/Emphasis><Subscript><Emphasis Type=\"Italic\">i<\/Emphasis><\/Subscript> is the invocation time,<Emphasis Type=\"Italic\"> D<\/Emphasis><Subscript><Emphasis Type=\"Italic\">i<\/Emphasis><\/Subscript> is the absolute deadline and<Emphasis Type=\"Italic\"> C<\/Emphasis><Subscript><Emphasis Type=\"Italic\">i<\/Emphasis><\/Subscript> is the WCET).","order":4,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}