{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T13:18:42Z","timestamp":1762003122045,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319747804"},{"type":"electronic","value":"9783319747811"}],"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-319-74781-1_21","type":"book-chapter","created":{"date-parts":[[2018,2,1]],"date-time":"2018-02-01T15:22:24Z","timestamp":1517498544000},"page":"300-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Integrated Simulation and Formal Verification of a Simple Autonomous Vehicle"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0685-2864","authenticated-orcid":false,"given":"Andrea","family":"Domenici","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9943-1975","authenticated-orcid":false,"given":"Adriano","family":"Fagiolini","sequence":"additional","affiliation":[]},{"given":"Maurizio","family":"Palmieri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,2,2]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","unstructured":"Attarzadeh-Niaki, S.H., Sander, I.: Co-simulation of embedded systems in a heterogeneous MoC-based modeling framework. In: 2011 6th IEEE International Symposium on Industrial and Embedded Systems, pp. 238\u2013247, June 2011. https:\/\/doi.org\/10.1109\/SIES.2011.5953667","DOI":"10.1109\/SIES.2011.5953667"},{"issue":"9","key":"21_CR2","doi-asserted-by":"publisher","first-page":"1342","DOI":"10.1109\/TCAD.2014.2329419","volume":"33","author":"C Bernardeschi","year":"2014","unstructured":"Bernardeschi, C., Cassano, L., Domenici, A., Sterpone, L.: ASSESS: a simulator of soft errors in the configuration memory of SRAM-based FPGAs. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 33(9), 1342\u20131355 (2014). https:\/\/doi.org\/10.1109\/TCAD.2014.2329419","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."},{"issue":"10, Part D","key":"21_CR3","doi-asserted-by":"publisher","first-page":"1243","DOI":"10.1016\/j.sysarc.2013.10.006","volume":"59","author":"C Bernardeschi","year":"2013","unstructured":"Bernardeschi, C., Cassano, L., Cimino, M.G., Domenici, A.: GABES: a genetic algorithm based environment for SEU testing in SRAM-FPGAs. J. Syst. Archit. 59(10, Part D), 1243\u20131254 (2013). https:\/\/doi.org\/10.1016\/j.sysarc.2013.10.006","journal-title":"J. Syst. Archit."},{"issue":"6","key":"21_CR4","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/j.ipl.2016.02.001","volume":"116","author":"C Bernardeschi","year":"2016","unstructured":"Bernardeschi, C., Domenici, A.: Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System. Inf. Process. Lett. 116(6), 409\u2013415 (2016). https:\/\/doi.org\/10.1016\/j.ipl.2016.02.001","journal-title":"Inf. Process. Lett."},{"issue":"99","key":"21_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TSE.2017.2694423","volume":"PP","author":"C Bernardeschi","year":"2017","unstructured":"Bernardeschi, C., Domenici, A., Masci, P.: A PVS-simulink integrated environment for model-based analysis of cyber-physical systems. IEEE Trans. Softw. Eng. PP(99), 1 (2017). https:\/\/doi.org\/10.1109\/TSE.2017.2694423","journal-title":"IEEE Trans. Softw. Eng."},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Blochwitz, T., Otter, M., Arnold, M., Bausch, C., Clau\u00df, C., Elmqvist, H., Junghanns, A., Mau\u00df, J., Monteiro, M., Neidhold, T., Neumerkel, D., Olsson, H., Peetz, J.V., Wolf, S.: The functional mockup interface for tool independent exchange of simulation models. In: Proceedings of the 8th International Modelica Conference, pp. 105\u2013114. Link\u00f6ping University Electronic Press (2011). https:\/\/doi.org\/10.3384\/ecp11063105","DOI":"10.3384\/ecp11063105"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/3-540-44659-1_6","volume-title":"Theorem Proving in Higher Order Logics","author":"V Carre\u00f1o","year":"2000","unstructured":"Carre\u00f1o, V., Mu\u00f1oz, C.: Aircraft trajectory modeling and alerting algorithm verification. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 90\u2013105. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44659-1_6"},{"key":"21_CR8","unstructured":"Di Vito, B.: Manip User\u2019s Guide, Version 1.3. http:\/\/shemesh.larc.nasa.gov\/people\/bld\/ftp\/manip-guide-1.3.pdf . Accessed 18 Aug 2015"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/BFb0105402","volume-title":"Theorem Proving in Higher Order Logics","author":"B Dutertre","year":"1996","unstructured":"Dutertre, B.: Elements of mathematical analysis in PVS. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 141\u2013156. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0105402"},{"key":"21_CR10","doi-asserted-by":"publisher","DOI":"10.1002\/9780470050118.ecse447","volume-title":"Vienna Development Method","author":"JS Fitzgerald","year":"2007","unstructured":"Fitzgerald, J.S., Larsen, P.G., Verhoef, M.: Vienna Development Method. Wiley, Hoboken (2007). https:\/\/doi.org\/10.1002\/9780470050118.ecse447"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Gomes, C., Thule, C., Broman, D., Larsen, P.G., Vangheluwe, H.: Co-simulation: state of the art. ACM Comput. Surv. (2017, to appear)","DOI":"10.1145\/3179993"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-44659-1_13","volume-title":"Theorem Proving in Higher Order Logics","author":"H Gottliebsen","year":"2000","unstructured":"Gottliebsen, H.: Transcendental functions and continuity checking in PVS. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 197\u2013214. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44659-1_13"},{"key":"21_CR14","volume-title":"Analysis and Simulation of Multiport Systems; The Bond Graph Approach to Physical System Dynamics","author":"D Karnopp","year":"1968","unstructured":"Karnopp, D., Rosenberg, R.: Analysis and Simulation of Multiport Systems; The Bond Graph Approach to Physical System Dynamics. M.I.T. Press, Cambridge (1968)"},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"Larsen, P.G., Fitzgerald, J., Woodcock, J., Fritzson, P., Brauer, J., Kleijn, C., Lecomte, T., Pfeil, M., Green, O., Basagiannis, S., Sadovykh, A.: 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":"21_CR16","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-642-54118-6_5","volume-title":"Collaborative Design for Embedded Systems. Co-modelling and Co-simulation","author":"PG Larsen","year":"2014","unstructured":"Larsen, P.G., Gamble, C., Pierce, K., Ribeiro, A., Lausdahl, K.: Support for co-modelling and co-simulation: the crescendo tool. In: Fitzgerald, J., Larsen, P.G., Verhoef, M. (eds.) Collaborative Design for Embedded Systems. Co-modelling and Co-simulation, pp. 97\u2013114. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54118-6_5"},{"issue":"12","key":"21_CR17","doi-asserted-by":"publisher","first-page":"1217","DOI":"10.1109\/43.736561","volume":"17","author":"EA Lee","year":"1998","unstructured":"Lee, E.A., Sangiovanni-Vincentelli, A.: A framework for comparing models of computation. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 17(12), 1217\u20131229 (1998). https:\/\/doi.org\/10.1109\/43.736561","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-319-21690-4_30","volume-title":"Computer Aided Verification","author":"P Masci","year":"2015","unstructured":"Masci, P., Oladimeji, P., Zhang, Y., Jones, P., Curzon, P., Thimbleby, H.: PVSio-web 2.0: joining PVS to HCI. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 470\u2013478. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_30"},{"key":"21_CR19","unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS. Technical Report, NIA 2003-03, NASA\/CR-2003-212418, National Institute of Aerospace, Hampton, VA, USA (2003)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., Narkawicz, A., Hagen, G., Upchurch, J., Dutle, A., Consiglio, M.: DAIDALUS: detect and avoid alerting logic for unmanned systems. In: Proceedings of the 34th Digital Avionics Systems Conference (DASC 2015) (2015)","DOI":"10.1109\/DASC.2015.7311588"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: PVSio-web: a tool for rapid prototyping device user interfaces in PVS. In: FMIS2013, 5th International Workshop on Formal Methods for Interactive Systems, London, UK, 24 June 2013. https:\/\/doi.org\/10.14279\/tuj.eceasst.69.963.944","DOI":"10.14279\/tuj.eceasst.69.963.944"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411\u2013414. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_91"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/3-540-59047-1_53","volume-title":"Theorem Provers in Circuit Design","author":"S Owre","year":"1995","unstructured":"Owre, S., Rushby, J.M., Shankar, N., Srivas, M.K.: A tutorial on using PVS for hardware verification. In: Kumar, R., Kropf, T. (eds.) TPCD 1994. LNCS, vol. 901, pp. 258\u2013279. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59047-1_53"},{"key":"21_CR24","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logics of dynamical systems. In: Proceedings of the 2012 27th Annual IEEE\/ACM Symposium on Logic in Computer Science, LICS 2012, pp. 13\u201324. IEEE Computer Society, Washington (2012). https:\/\/doi.org\/10.1109\/LICS.2012.13","DOI":"10.1109\/LICS.2012.13"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/3-540-44667-2_9","volume-title":"Lectures on Formal Methods and PerformanceAnalysis","author":"WH Sanders","year":"2001","unstructured":"Sanders, W.H., Meyer, J.F.: Stochastic activity networks: formal definitions and concepts*. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000. LNCS, vol. 2090, pp. 315\u2013343. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44667-2_9"},{"key":"21_CR26","volume-title":"First-Order Logic","author":"RM Smullyan","year":"1995","unstructured":"Smullyan, R.M.: First-Order Logic. Dover Publications, New York (1995)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-74781-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T04:19:38Z","timestamp":1570681178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-74781-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319747804","9783319747811"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-74781-1_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}