{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:22:42Z","timestamp":1725988962692},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030002435"},{"type":"electronic","value":"9783030002442"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-00244-2_2","type":"book-chapter","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T00:12:38Z","timestamp":1535587958000},"page":"19-31","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Building Correct Cyber-Physical Systems: Why We Need a Multiview Contract Theory"],"prefix":"10.1007","author":[{"given":"Susanne","family":"Graf","sequence":"first","affiliation":[]},{"given":"Sophie","family":"Quinton","sequence":"additional","affiliation":[]},{"given":"Alain","family":"Girault","sequence":"additional","affiliation":[]},{"given":"Gregor","family":"G\u00f6ssler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"key":"2_CR1","unstructured":"aiT. https:\/\/www.absint.com\/ait\/"},{"key":"2_CR2","unstructured":"RT-Druid. http:\/\/www.evidence.eu.com\/products\/rt-druid.html"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Al Khatib, M., Girard, A., Dang, T.: Scheduling of embedded controllers under timing contracts. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017. ACM, New York (2017)","DOI":"10.1145\/3049797.3049816"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365\u2013370. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_30"},{"issue":"3","key":"2_CR5","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10009-012-0263-9","volume":"15","author":"I Assayad","year":"2013","unstructured":"Assayad, I., Girault, A., Kalla, H.: Tradeoff exploration between reliability, power consumption, and execution time for embedded systems. Int. J. Software Tools Technol. Transfer 15(3), 229\u2013243 (2013)","journal-title":"Int. J. Software Tools Technol. Transfer"},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/TDSC.2004.2","volume":"1","author":"A Avizienis","year":"2004","unstructured":"Avizienis, A., Laprie, J.-C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secure Comput. 1(1), 11\u201333 (2004)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Axer, P., Ernst, R.: Stochastic response-time guarantee for non-preemptive, fixed-priority scheduling under errors. In: The 50th Annual Design Automation Conference 2013, DAC 2013, Austin, TX, USA, 29 May\u201307 June 2013. ACM (2013)","DOI":"10.1145\/2463209.2488946"},{"issue":"4","key":"2_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/MC.2003.1193228","volume":"36","author":"F Balarin","year":"2003","unstructured":"Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A.: Metropolis: an integrated electronic system design environment. Computer 36(4), 45\u201352 (2003)","journal-title":"Computer"},{"issue":"3","key":"2_CR9","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Software 28(3), 41\u201348 (2011)","journal-title":"IEEE Software"},{"issue":"4","key":"2_CR10","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/1376804.1376811","volume":"7","author":"A Benveniste","year":"2008","unstructured":"Benveniste, A., Caillaud, B., Carloni, L.P., Caspi, P., Sangiovanni-Vincentelli, A.L.: Composing heterogeneous reactive systems. ACM Trans. Embedded Comput. Syst. 7(4), 43 (2008)","journal-title":"ACM Trans. Embedded Comput. Syst."},{"issue":"2\u20133","key":"2_CR11","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Design Autom. 12(2\u20133), 124\u2013400 (2018)","journal-title":"Found. Trends Electron. Design Autom."},{"key":"2_CR12","unstructured":"Bhat, A., Samii, S., Rajkumar, R.R.: Recovery time considerations in real-time systems employing software fault tolerance. In: Altmeyer, S. (ed.) 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), vol. 106. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)"},{"key":"2_CR13","unstructured":"Bri\u00e8re, D., Ribot, D., Pilaud, D., Camus, J.-L.: Methods and specifications tools for Airbus on-board systems. In: Avionics Conference and Exhibition, London, UK. ERA Technology (1994)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-13754-9_6","volume-title":"Time for Verification","author":"W Damm","year":"2010","unstructured":"Damm, W., Dierks, H., Oehlerking, J., Pnueli, A.: Towards component based design of hybrid systems: safety and stability. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 96\u2013143. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13754-9_6"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Derler, P., Lee, E., Tripakis, S., T\u00f6rngren, M.: Cyber-physical system design contracts. In: Proceedings of the ACM\/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013. ACM, New York (2013)","DOI":"10.1145\/2502524.2502540"},{"key":"2_CR16","unstructured":"Ernst, R., Henia, R., Quinton, S.: Beyond the deadline: new interfaces between control and scheduling for the design and analysis of critical embedded systems. Tutorial at ESWeek (2017)"},{"key":"2_CR17","unstructured":"Fellmuth, J., G\u00f6thel, T., Glesner, S.: Instruction caches in static WCET analysis of artificially diversified software. In: Altmeyer, S. (ed.) 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), vol. 106. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)"},{"issue":"8","key":"2_CR18","doi-asserted-by":"publisher","first-page":"2330","DOI":"10.1016\/j.automatica.2013.04.036","volume":"49","author":"D Fontanelli","year":"2013","unstructured":"Fontanelli, D., Greco, L., Palopoli, L.: Soft real-time scheduling for embedded control systems. Automatica 49(8), 2330\u20132338 (2013)","journal-title":"Automatica"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258\u2013273. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31954-2_17"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Frehse, G., Hamann, A., Quinton, S., Woehrle, M.: Formal analysis of timing effects on closed-loop properties of control software. In: Proceedings of the IEEE 35th IEEE Real-Time Systems Symposium, RTSS 2014, Rome, Italy, 2\u20135 December 2014. IEEE Computer Society (2014)","DOI":"10.1109\/RTSS.2014.28"},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/311531.311532","volume":"31","author":"F G\u00e4rtner","year":"1999","unstructured":"G\u00e4rtner, F.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Comput. Surv. 31(1), 1\u201326 (1999)","journal-title":"ACM Comput. Surv."},{"issue":"4","key":"2_CR22","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/TDSC.2008.50","volume":"6","author":"A Girault","year":"2009","unstructured":"Girault, A., Kalla, H.: A novel bicriteria scheduling heuristics providing a guaranteed global system failure rate. IEEE Trans. Dependable Secure Comput. 6(4), 241\u2013254 (2009)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"2_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-3879-3_8","volume-title":"Embedded Systems Development: From Functional Models to Implementations","author":"S Graf","year":"2014","unstructured":"Graf, S., Passerone, R., Quinton, S.: Contract-based reasoning for component systems with rich interactions. In: Sangiovanni-Vincentelli, A.L., Zeng, H., Natale, M.D., Marwedel, P. (eds.) Embedded Systems Development: From Functional Models to Implementations. Springer, New York (2014). https:\/\/doi.org\/10.1007\/978-1-4614-3879-3_8"},{"key":"2_CR24","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) Computer-Aided Verification, Proceedings of a DIMACS Workshop 1990, New Brunswick, New Jersey, USA, 18\u201321 June 1990, vol. 3. DIMACS Series in Discrete Mathematics and Theoretical Computer Science (1990)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Henia, R., Hamann, A., Jersak, M., Racu, R., Richter, K., Ernst, R.: System level performance analysis\u2013the symta\/s approach. In: IEE Proceedings - Computers and Digital Techniques, vol. 152 (2005)","DOI":"10.1049\/ip-cdt:20045088"},{"key":"2_CR26","unstructured":"Kr\u00fcger, K., V\u00f6lp, M., Fohler, G.: Vulnerability analysis and mitigation of directed timing inference based attacks on time-triggered systems. In: Altmeyer, S. (ed.) 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), vol. 106. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Kumar, P., Goswami, D., Chakraborty, S., Annaswamy, A., Lampka, K., Thiele, L.: A hybrid approach to cyber-physical systems verification. In: Proceedings of the 49th Annual Design Automation Conference, DAC 2012. ACM (2012)","DOI":"10.1145\/2228360.2228484"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Li, J., Nuzzo, P., Sangiovanni-Vincentelli, A., Xi, Y., Li, D.: Stochastic contracts for cyber-physical system design under probabilistic requirements. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, New York, NY, USA. ACM (2017)","DOI":"10.1145\/3127041.3127045"},{"issue":"1","key":"2_CR29","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Design 6(1), 11\u201344 (1995)","journal-title":"Formal Methods Syst. Design"},{"issue":"10","key":"2_CR30","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Computer 25(10), 40\u201351 (1992)","journal-title":"IEEE Computer"},{"issue":"4","key":"2_CR31","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Software Eng."},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-662-54494-5_8","volume-title":"Fundamental Approaches to Software Engineering","author":"A M\u00fcller","year":"2017","unstructured":"M\u00fcller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: Change and delay contracts for hybrid system component verification. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 134\u2013151. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54494-5_8"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Otter, M., Mattsson, S., Elmqvist, H.: Multidomain modeling with Modelica. In: Handbook of Dynamic System Modeling. Chapmanand Hall\/CRC (2007)","DOI":"10.1201\/9781420010855.pt5"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Passerone, R., et al.: Metamodels in Europe: languages, tools, and applications. IEEE Des. Test Comput. 26(3) (2009)","DOI":"10.1109\/MDT.2009.64"},{"issue":"1","key":"2_CR35","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1243\/09544062JMES2105","volume":"225","author":"GAP Castaneda","year":"2011","unstructured":"Castaneda, G.A.P., Aubry, J.-F., Brinzei, N.: Stochastic hybrid automata model for dynamic reliability assessment. Proc. Inst. Mech. Eng. Part O J. Risk Reliab. 225(1), 28\u201341 (2011)","journal-title":"Proc. Inst. Mech. Eng. Part O J. Risk Reliab."},{"key":"2_CR36","series-title":"NATO ASI Series (Series F: Computer and Systems Sciences)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and Models of Concurrent Systems","author":"A Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 13. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_5"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Powell, D.: Failure mode assumption and assumption coverage. In: International Symposium on Fault-Tolerant Computing, FTCS-22, Boston, MA, USA. IEEE. Research report LAAS 91462 (1992)","DOI":"10.1109\/FTCS.1992.243562"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-54862-8_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Reineke","year":"2014","unstructured":"Reineke, J., Tripakis, S.: Basic problems in multi-view modeling. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 217\u2013232. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_15"},{"issue":"2","key":"2_CR39","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/2948973","volume":"3","author":"H Sheikh","year":"2016","unstructured":"Sheikh, H., Ahmad, I.: Sixteen heuristics for joint optimization of performance, energy, and temperature in allocating tasks to multi-cores. ACM Trans. Parallel Comput. 3(2), 9 (2016)","journal-title":"ACM Trans. Parallel Comput."},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0023444","volume-title":"STACS 97","author":"B Steffen","year":"1997","unstructured":"Steffen, B.: Unifying models. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 1\u201320. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0023444"},{"key":"2_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and Control of Hybrid Systems - A Symbolic Approach","author":"P Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems - A Symbolic Approach. Springer, New York (2009). https:\/\/doi.org\/10.1007\/978-1-4419-0224-5"},{"issue":"2\/3","key":"2_CR42","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008141130870","volume":"18","author":"H Theiling","year":"2000","unstructured":"Theiling, H., Ferdinand, C., Wilhelm, R.: Fast and precise WCET prediction by separated cache and path analyses. Real-Time Syst. 18(2\/3), 157\u2013179 (2000)","journal-title":"Real-Time Syst."},{"issue":"2","key":"2_CR43","first-page":"118","volume":"25","author":"Y Zhao","year":"2010","unstructured":"Zhao, Y., Xiong, Y., Lee, E.A., Liu, X., Zhong, L.C.: The design and application of structured types in ptolemy II. Int. J. Intell. Syst. 25(2), 118\u2013136 (2010)","journal-title":"Int. J. Intell. Syst."},{"key":"2_CR44","unstructured":"Zhu, D., Melhem, R., Moss\u00e9, D.: The effects of energy management on reliability in real-time embedded systems. In: International Conference on Computer Aided Design, ICCAD 2004, San Jose, CA, USA (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00244-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T02:01:27Z","timestamp":1571796087000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00244-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030002435","9783030002442"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00244-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}