{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,8]],"date-time":"2024-05-08T05:10:20Z","timestamp":1715145020209},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,3,31]],"date-time":"2013-03-31T00:00:00Z","timestamp":1364688000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s10009-013-0271-4","type":"journal-article","created":{"date-parts":[[2013,3,30]],"date-time":"2013-03-30T18:46:35Z","timestamp":1364669195000},"page":"149-154","source":"Crossref","is-referenced-by-count":1,"title":["Rigorous embedded design: challenges and perspectives"],"prefix":"10.1007","volume":"15","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,3,31]]},"reference":[{"key":"271_CR1","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"271_CR2","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.-H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011)","journal-title":"IEEE Softw."},{"key":"271_CR3","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Peled, D.: Efficient deadlock detection for concurrent systems. In: MEMOCODE, pp. 119\u2013129, IEEE (2011)","DOI":"10.1109\/MEMCOD.2011.5970518"},{"key":"271_CR4","doi-asserted-by":"crossref","unstructured":"Bourgos, P., Basu, A., Bozga, M., Bensalem, S., Sifakis, J., Huang, K.: Rigorous system level modeling and analysis of mixed HW\/SW systems. In: MEMOCODE, pp. 11\u201320. IEEE (2011)","DOI":"10.1109\/MEMCOD.2011.5970506"},{"key":"271_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/b106761","volume-title":"Embedded systems design: the ARTIST roadmap for research and development, volume 3,436 of LNCS","author":"B Bouyssounouse","year":"2005","unstructured":"Bouyssounouse, B., Sifakis, J.: Embedded systems design: the ARTIST roadmap for research and development, volume 3,436 of LNCS. Springer, New York (2005)"},{"key":"271_CR6","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press, Cambridge (1999)"},{"issue":"2","key":"271_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1348250.1348253","volume":"17","author":"JM Cobleigh","year":"2008","unstructured":"Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: an evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2), 1\u201352 (2008)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"271_CR8","doi-asserted-by":"crossref","unstructured":"Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: TACAS, pp. 331\u2013346 (2003)","DOI":"10.1007\/3-540-36577-X_24"},{"key":"271_CR9","doi-asserted-by":"crossref","unstructured":"Craciunas, S., Kirsch, C., Payer, H., Roeck, H., Sokolova, A.: Temporal isolation in real-time systems: the VBS approach (2013, in this issue)","DOI":"10.1007\/s10009-012-0246-x"},{"key":"271_CR10","unstructured":"Dalsgaard, A.E., Olesen, M.C., Toft, M., Hansen, R.R., Larsen, K.G.: METAMOC: modular execution time analysis using model checking. In: WCET, volume 15 of OASICS, pp. 113\u2013123. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2010)"},{"key":"271_CR11","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I\/O automata: a complete specification theory for real-time systems. In: HSCC, pp. 91\u2013100. ACM (2010)","DOI":"10.1145\/1755952.1755967"},{"key":"271_CR12","volume-title":"Concurrency verification: introduction to compositional and noncompositional methods","author":"W-P Roever de","year":"2000","unstructured":"de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency verification: introduction to compositional and noncompositional methods. Cambridge University Press, Cambridge (2000)"},{"key":"271_CR13","doi-asserted-by":"crossref","unstructured":"Farzan, A., Chen, Y.-F., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Extending automated compositional verification to the full class of omega-regular languages. In: TACAS, pp. 2\u201317. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_2"},{"key":"271_CR14","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption generation for software component verification. In: ASE, pp. 3\u201312. IEEE Computer Society (2002)","DOI":"10.1109\/ASE.2002.1114984"},{"key":"271_CR15","doi-asserted-by":"crossref","unstructured":"Girault, A., Assayad, I., Kalla, H.: Tradeoff exploration between reliability, power consumption, and execution time for embedded systems (2013, in this issue)","DOI":"10.1007\/s10009-012-0263-9"},{"key":"271_CR16","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: methodology and case studies. In: CAV, pp. 440\u2013451. Springer (1998)","DOI":"10.1007\/BFb0028765"},{"key":"271_CR17","doi-asserted-by":"crossref","unstructured":"Lampka, K., Perathoner, S., Thiele, L.: Analytic real-time analysis and timed automata: a hybrid method for analyzing embedded real-time systems. In: EMSOFT, pp. 107\u2013116. ACM (2009)","DOI":"10.1145\/1629335.1629351"},{"key":"271_CR18","doi-asserted-by":"crossref","unstructured":"Lampka, K., Perathoner, S., Thiele, L.: Featuring component-oriented design of systems: analytic real-time interfaces for state-based component implementations (2013, in this issue)","DOI":"10.1007\/s10009-012-0257-7"},{"key":"271_CR19","unstructured":"Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits (2013, in this issue)"},{"key":"271_CR20","doi-asserted-by":"crossref","unstructured":"Moser, C., Chen, J.-J., Thiele, L.: An energy management framework for energy harvesting embedded systems. J. Emerg. Technol. 6(2) (2010)","DOI":"10.1145\/1773814.1773818"},{"key":"271_CR21","unstructured":"Palopoli, L., Le, T.T.H., Passerone, R., Ramadian, Y.: Timed-automata based schedulability analysis for distributed firm real-time systems: a case study (2013, in this issue)"},{"key":"271_CR22","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume":"F13","author":"A Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. Logics Models Concurr. Syst. F13, 123\u2013144 (1985)","journal-title":"Logics Models Concurr. Syst."},{"key":"271_CR23","doi-asserted-by":"crossref","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: 5th international symposium on programming, pp. 337\u2013351. Springer (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"271_CR24","doi-asserted-by":"crossref","unstructured":"Rox, J., Ernst, R.: Using compositional performance analysis for obtaining viable end-to-end latencies in distributed embedded systems (2013, in this issue)","DOI":"10.1007\/s10009-012-0260-z"},{"key":"271_CR25","doi-asserted-by":"crossref","unstructured":"Thiele, L., Schor, L., Yang, H., Bacivarov, I.: Thermal-aware system analysis and software synthesis for embedded multi-processors. In: DAC, pp. 268\u2013273. ACM (2011)","DOI":"10.1145\/2024724.2024786"},{"key":"271_CR26","doi-asserted-by":"crossref","unstructured":"Thiele, L., Wandeler, E., Stoimenov, N.: Real-time interfaces for composing real-time systems. In: EMSOFT, pp. 34\u201343. ACM (2006)","DOI":"10.1145\/1176887.1176894"},{"key":"271_CR27","unstructured":"Vaandrager, F., Igna, G., Houben, F.: Modeling task systems using parameterized partial orders (2013, in this issue)"}],"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-013-0271-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0271-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0271-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,8]],"date-time":"2024-05-08T04:46:19Z","timestamp":1715143579000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0271-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,31]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["271"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0271-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,31]]}}}