{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T00:54:00Z","timestamp":1743123240311,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030672195"},{"type":"electronic","value":"9783030672201"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-67220-1_20","type":"book-chapter","created":{"date-parts":[[2021,1,16]],"date-time":"2021-01-16T08:03:07Z","timestamp":1610784187000},"page":"263-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Cross-level Co-simulation and Verification of an Automatic Transmission Control on Embedded Processor"],"prefix":"10.1007","author":[{"given":"Cinzia","family":"Bernardeschi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Domenici","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maurizio","family":"Palmieri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Saponara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tanguy","family":"Sassolas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arief","family":"Wicaksana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lilia","family":"Zaourar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,17]]},"reference":[{"key":"20_CR1","unstructured":"Accelera: TLM-2.0 Language Reference Manual (2009). https:\/\/www.accellera.org\/images\/downloads\/standards\/systemc\/TLM_2_0_LRM.pdf"},{"key":"20_CR2","unstructured":"Bellard, F.: QEMU, a fast and portable dynamic translator. In: Proceedings of the Annual Conference on USENIX Annual Technical Conference, ATEC 2005, p. 41. USENIX Association, USA (2005)"},{"issue":"6","key":"20_CR3","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1109\/TSE.2017.2694423","volume":"44","author":"C Bernardeschi","year":"2018","unstructured":"Bernardeschi, C., Domenici, A., Masci, P.: A PVS-simulink integrated environment for model-based analysis of cyber-physical systems. IEEE Trans. Softw. Eng. 44(6), 512\u2013533 (2018)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Blochwitz, T., et al.: Functional mockup interface 2.0: the standard for tool independent exchange of simulation models. In: Proceedings of the 9th International MODELICA Conference, pp. 173\u2013184. No. 76 in Link\u00f6ping Electronic Conference Proceedings (2012)","DOI":"10.3384\/ecp12076173"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Bohrer, B., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 208\u2013221. ACM (2017). https:\/\/doi.org\/10.1145\/3018610.3018616","DOI":"10.1145\/3018610.3018616"},{"key":"20_CR6","doi-asserted-by":"publisher","unstructured":"Charif, A., Busnot, G., Mameesh, R.H., Sassolas, T., Ventroux, N.: Fast virtual prototyping for embedded computing systems design and exploration. In: Chillet, D. (ed.) Proceedings of the Rapid Simulation and Performance Evaluation: Methods and Tools, RAPIDO 2019, Valencia, Spain, 21\u201323 January 2019, pp. 3:1\u20133:8. ACM (2019). https:\/\/doi.org\/10.1145\/3300189.3300192","DOI":"10.1145\/3300189.3300192"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52\u201367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_4"},{"issue":"9","key":"20_CR8","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L De Moura","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-319-74781-1_21","volume-title":"Software Engineering and Formal Methods","author":"A Domenici","year":"2018","unstructured":"Domenici, A., Fagiolini, A., Palmieri, M.: Integrated simulation and formal verification of a simple autonomous vehicle. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 300\u2013314. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-74781-1_21"},{"issue":"2","key":"20_CR10","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/MCS.2016.2643244","volume":"37","author":"F Franchetti","year":"2017","unstructured":"Franchetti, F., et al.: High-assurance spiral: end-to-end guarantees for robot and car control. IEEE Control Syst. 37(2), 82\u2013103 (2017). https:\/\/doi.org\/10.1109\/MCS.2016.2643244","journal-title":"IEEE Control Syst."},{"issue":"3","key":"20_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3179993","volume":"51","author":"C Gomes","year":"2018","unstructured":"Gomes, C., Thule, C., Broman, D., Larsen, P.G., Vangheluwe, H.: Co-simulation: a survey. ACM Comput. Surv. (CSUR) 51(3), 1\u201333 (2018)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"20_CR12","series-title":"NATO ASI Series (Series F: Computer and Systems Sciences)","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-642-59615-5_13"},{"key":"20_CR13","unstructured":"IEEE: IEEE Standard for Standard SystemC Language Reference Manual. IEEE Std 1666\u20132011 (Revision of IEEE Std 1666\u20132005), pp. 1\u2013638 (2012)"},{"key":"20_CR14","unstructured":"Imperas Ltd.: Open Virtual Platforms (2020). http:\/\/www.ovpworld.org\/"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Larsen, P.G., et al.: Integrated tool chain for model-based design of Cyber-Physical Systems: the INTO-CPS project. In: 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data), pp. 1\u20136, April 2016. https:\/\/doi.org\/10.1109\/CPSData.2016.7496424","DOI":"10.1109\/CPSData.2016.7496424"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-319-06200-6_16","volume-title":"NASA Formal Methods","author":"P Masci","year":"2014","unstructured":"Masci, P., et al.: Combining PVSio with Stateflow. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 209\u2013214. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_16"},{"key":"20_CR17","doi-asserted-by":"publisher","unstructured":"Mauro, G., Thimbleby, H., Domenici, A., Bernardeschi, C.: Extending a user interface prototyping tool with automatic MISRA C code generation. In: Dubois, C., Masci, P., M\u00e9ry, D. (eds.) Third Workshop on Formal Integrated Development Environments. Electronic Proceedings in Theoretical Computer Science, vol. 240, pp. 53\u201366. Open Publishing Association (2017). https:\/\/doi.org\/10.4204\/EPTCS.240.4","DOI":"10.4204\/EPTCS.240.4"},{"key":"20_CR18","unstructured":"Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: PVSio-web: a tool for rapid prototyping device user interfaces in PVS. In: FMIS 2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, 24 June 2013 (2013)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"issue":"3","key":"20_CR20","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1007\/s10270-019-00754-9","volume":"19","author":"M Palmieri","year":"2020","unstructured":"Palmieri, M., Bernardeschi, C., Masci, P.: A framework for FMI-based co-simulation of human-machine interfaces. Softw. Syst. Model. 19(3), 601\u2013623 (2020)","journal-title":"Softw. Syst. Model."},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-030-57506-9_3","volume-title":"Software Engineering and Formal Methods","author":"M Palmieri","year":"2020","unstructured":"Palmieri, M., Macedo, H.D.: Automatic generation of functional mock-up units from formal specifications. In: Camara, J., Steffen, M. (eds.) SEFM 2019. LNCS, vol. 12226, pp. 27\u201333. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57506-9_3"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_15"},{"issue":"2","key":"20_CR23","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1109\/JPROC.2004.840306","volume":"93","author":"M P\u00fcschel","year":"2005","unstructured":"P\u00fcschel, M., et al.: SPIRAL: code generation for DSP transforms. Proc. IEEE 93(2), 232\u2013275 (2005). https:\/\/doi.org\/10.1109\/JPROC.2004.840306","journal-title":"Proc. IEEE"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Saidi, S.E., Charif, A., Sassolas, T., Le Guay, P.G., Souza, H.V., Ventroux, N.: Fast virtual prototyping of cyber-physical systems using SystemC and FMI: ADAS use case. In: Proceedings of the 30th International Workshop on Rapid System Prototyping (RSP 2019), pp. 43\u201349 (2019)","DOI":"10.1145\/3339985.3358488"},{"issue":"5","key":"20_CR25","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/MS.2003.1231146","volume":"20","author":"B Selic","year":"2003","unstructured":"Selic, B.: The pragmatics of model-driven development. IEEE Softw. 20(5), 19\u201325 (2003). https:\/\/doi.org\/10.1109\/MS.2003.1231146","journal-title":"IEEE Softw."},{"key":"20_CR26","unstructured":"Synopsys: Virtualizer (2020). https:\/\/www.synopsys.com\/verification\/virtual-prototyping\/virtualizer.html"},{"key":"20_CR27","doi-asserted-by":"publisher","unstructured":"Ventroux, N., et al.: SESAM: an MPSoC simulation environment for dynamic application processing. In: 2010 10th IEEE International Conference on Computer and Information Technology, pp. 1880\u20131886 (2010). https:\/\/doi.org\/10.1109\/CIT.2010.322","DOI":"10.1109\/CIT.2010.322"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67220-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,16]],"date-time":"2021-01-16T08:20:16Z","timestamp":1610785216000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-67220-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030672195","9783030672201"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-67220-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"17 January 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/event.cwi.nl\/sefm2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}