{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,26]],"date-time":"2025-09-26T00:07:01Z","timestamp":1758845221043,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T00:00:00Z","timestamp":1578528000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T00:00:00Z","timestamp":1578528000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"CrossLab project","award":["Italian Ministry of Education and Research"],"award-info":[{"award-number":["Italian Ministry of Education and Research"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Comput Virol Hack Tech"],"published-print":{"date-parts":[[2020,3]]},"DOI":"10.1007\/s11416-019-00344-9","type":"journal-article","created":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T12:02:38Z","timestamp":1578571358000},"page":"63-77","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Formalization and co-simulation of attacks on cyber-physical systems"],"prefix":"10.1007","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1604-4465","authenticated-orcid":false,"given":"Cinzia","family":"Bernardeschi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0685-2864","authenticated-orcid":false,"given":"Andrea","family":"Domenici","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6177-0928","authenticated-orcid":false,"given":"Maurizio","family":"Palmieri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,1,9]]},"reference":[{"key":"344_CR1","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/j.compind.2018.04.017","volume":"100","author":"R Alguliyev","year":"2018","unstructured":"Alguliyev, R., Imamverdiyev, Y., Sukhostat, L.: Cyber-physical systems and their security issues. Computers in Industry 100, 212\u2013223 (2018). https:\/\/doi.org\/10.1016\/j.compind.2018.04.017","journal-title":"Computers in Industry"},{"issue":"2","key":"344_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"11","key":"344_CR3","doi-asserted-by":"publisher","first-page":"2479","DOI":"10.1016\/j.jss.2012.05.061","volume":"85","author":"M Avvenuti","year":"2012","unstructured":"Avvenuti, M., Bernardeschi, C., Francesco, N.D., Masci, P.: JCSI: A tool for checking secure information flow in java card applications. Journal of Systems and Software 85(11), 2479\u20132493 (2012). https:\/\/doi.org\/10.1016\/j.jss.2012.05.061","journal-title":"Journal of Systems and Software"},{"unstructured":"Bagnato, A., Brosse, E., Quadri, I., Sadovykh, A.: INTO-CPS: An integrated \u201ctool chain\u201d for comprehensive model-based design of cyber-physical systems (2015). This publication is part of the Horizon 2020 project: Integrated Tool chain for model-based design of CPSs (INTO-CPS), project\/GA number 644047","key":"344_CR4"},{"issue":"9","key":"344_CR5","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. on CAD of Integrated Circuits and Systems 33(9), 1342\u20131355 (2014). https:\/\/doi.org\/10.1109\/TCAD.2014.2329419","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"issue":"6","key":"344_CR6","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":"6","key":"344_CR7","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. Software Eng. 44(6), 512\u2013533 (2018). https:\/\/doi.org\/10.1109\/TSE.2017.2694423","journal-title":"IEEE Trans. Software Eng."},{"doi-asserted-by":"publisher","unstructured":"Blochwitz, T., Otter, M., Akesson, J., Arnold, M., Clau\u00df, C., Elmqvist, H., Friedrich, M., Junghanns, A., Mauss, J., Neumerkel, D., Olsson, H., Viel, A.: Functional Mockup Interface 2.0: The Standard for Tool independent Exchange of Simulation Models. In: Proceedings of the 9th International MODELICA Conference;September 3-5; 2012; Munich; Germany, no.\u00a076 in Link\u00f6ping Electronic Conference Proceedings, pp. 173\u2013184. Link\u00f6ping University Electronic Press (2012). https:\/\/doi.org\/10.3384\/ecp12076173","key":"344_CR8","DOI":"10.3384\/ecp12076173"},{"issue":"5","key":"344_CR9","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1016\/S0928-4869(99)00018-X","volume":"7","author":"JF Broenink","year":"1999","unstructured":"Broenink, J.F.: 20-SIM software for hierarchical bond-graph\/block-diagram models. Simulation Practice and Theory 7(5), 481\u2013492 (1999). https:\/\/doi.org\/10.1016\/S0928-4869(99)00018-X","journal-title":"Simulation Practice and Theory"},{"issue":"3","key":"344_CR10","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/j.ijcip.2012.08.002","volume":"5","author":"M Burmester","year":"2012","unstructured":"Burmester, M., Magkos, E., Chrissikopoulos, V.: Modeling security in cyber-physical systems. International Journal of Critical Infrastructure Protection 5(3), 118\u2013126 (2012). https:\/\/doi.org\/10.1016\/j.ijcip.2012.08.002","journal-title":"International Journal of Critical Infrastructure Protection"},{"key":"344_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Methods, Models and Tools for Fault Tolerance","year":"2009","unstructured":"Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.): Methods. Models and Tools for Fault Tolerance. Springer-Verlag, Berlin, Heidelberg (2009)"},{"key":"344_CR12","first-page":"141","volume-title":"Lecture Notes in Computer Science","author":"Bruno Dutertre","year":"1996","unstructured":"Dutertre, B.: Elements of mathematical analysis in pvs. In: Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs \u201996, pp. 141\u2013156. Springer-Verlag, Berlin, Heidelberg (1996)"},{"key":"344_CR13","doi-asserted-by":"publisher","DOI":"10.5220\/0005050003150320","author":"A Ferrante","year":"2014","unstructured":"Ferrante, A., Kaitovic, I., Milosevic, J.: Modelling requirements for security-enhanced design of embedded systems (2014). https:\/\/doi.org\/10.5220\/0005050003150320","journal-title":"Modelling requirements for security-enhanced design of embedded systems"},{"issue":"3","key":"344_CR14","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: Hysat: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design 30(3), 179\u2013198 (2007). https:\/\/doi.org\/10.1007\/s10703-006-0031-0","journal-title":"Formal Methods in System Design"},{"key":"344_CR15","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"Goran Frehse","year":"2011","unstructured":"Frehse, G., Le\u00a0Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: Spaceex: Scalable verification of hybrid systems. In: G.\u00a0Gopalakrishnan, S.\u00a0Qadeer (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV), no. 6806 in LNCS, pp. 379\u2013395. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"issue":"6","key":"344_CR16","doi-asserted-by":"publisher","first-page":"1802","DOI":"10.1109\/JIOT.2017.2703172","volume":"4","author":"A Humayed","year":"2017","unstructured":"Humayed, A., Lin, J., Li, F., Luo, B.: Cyber-Physical Systems Security\u2013A Survey. IEEE Internet of Things Journal 4(6), 1802\u20131831 (2017). https:\/\/doi.org\/10.1109\/JIOT.2017.2703172","journal-title":"IEEE Internet of Things Journal"},{"key":"344_CR17","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-662-46681-0_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Jean-Baptiste Jeannin","year":"2015","unstructured":"Jeannin, J., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: C.\u00a0Baier, C.\u00a0Tinelli (eds.) TACAS, LNCS, vol. 9035, pp. 21\u201336. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_2"},{"key":"344_CR18","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.psep.2016.05.001","volume":"102","author":"Y Khalil","year":"2016","unstructured":"Khalil, Y.: A novel probabilistically timed dynamic model for physical security attack scenarios on critical infrastructures. Process Safety and Environmental Protection 102, 473\u2013484 (2016). https:\/\/doi.org\/10.1016\/j.psep.2016.05.001","journal-title":"Process Safety and Environmental Protection"},{"key":"344_CR19","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-319-98938-9_17","volume-title":"Lecture Notes in Computer Science","author":"Ruggero Lanotte","year":"2018","unstructured":"Lanotte, R., Merro, M., Tini, S.: Towards a formal notion of impact metric for cyber-physical attacks. In: Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings, pp. 296\u2013315 (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_17"},{"issue":"1","key":"344_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1668862.1668864","volume":"35","author":"PG Larsen","year":"2010","unstructured":"Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The Overture Initiative Integrating Tools for VDM. SIGSOFT Softw. Eng. Notes 35(1), 1\u20136 (2010). https:\/\/doi.org\/10.1145\/1668862.1668864","journal-title":"SIGSOFT Softw. Eng. Notes"},{"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 (2016). https:\/\/doi.org\/10.1109\/CPSData.2016.7496424","key":"344_CR21","DOI":"10.1109\/CPSData.2016.7496424"},{"key":"344_CR22","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-319-06200-6_16","volume-title":"Lecture Notes in Computer Science","author":"Paolo Masci","year":"2014","unstructured":"Masci, P., Zhang, Y., Jones, P.L., Oladimeji, P., D\u2019Urso, E., Bernardeschi, C., Curzon, P., Thimbleby, H.: Combining PVSio with Stateflow. In: NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, pp. 209\u2013214 (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_16"},{"key":"344_CR23","doi-asserted-by":"publisher","first-page":"53","DOI":"10.4204\/EPTCS.240.4","volume":"240","author":"Gioacchino Mauro","year":"2017","unstructured":"Mauro, G., Thimbleby, H., Domenici, A., Bernardeschi, C.: Extending a user interface prototyping tool with automatic MISRA\u00a0C code generation. In: C.\u00a0Dubois, P.\u00a0Masci, D.\u00a0M\u00e9ry (eds.) Proceedings of the Third Workshop on Formal Integrated Development Environment, Limassol, Cyprus, November 8, 2016, Electronic Proceedings in Theoretical Computer Science, vol. 240, pp. 53\u201366. Open Publishing Association, (2017). https:\/\/doi.org\/10.4204\/EPTCS.240.4","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"1","key":"344_CR24","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/JSAC.2002.806125","volume":"21","author":"C Meadows","year":"2003","unstructured":"Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE Journal on Selected Areas in Communications 21(1), 44\u201354 (2003). https:\/\/doi.org\/10.1109\/JSAC.2002.806125","journal-title":"IEEE Journal on Selected Areas in Communications"},{"doi-asserted-by":"publisher","unstructured":"Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.: Hey malware, i can find you! pp. 261\u2013262 (2016). https:\/\/doi.org\/10.1109\/WETICE.2016.67","key":"344_CR25","DOI":"10.1109\/WETICE.2016.67"},{"issue":"1","key":"344_CR26","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1109\/TR.2015.2406860","volume":"65","author":"R Mitchell","year":"2016","unstructured":"Mitchell, R., Chen, I.: Modeling and analysis of attacks and counter defense mechanisms for cyber physical systems. IEEE Transactions on Reliability 65(1), 350\u2013358 (2016). https:\/\/doi.org\/10.1109\/TR.2015.2406860","journal-title":"IEEE Transactions on Reliability"},{"doi-asserted-by":"crossref","unstructured":"Mitsch, S., Ghorbal, K., Platzer, A.: On provably safe obstacle avoidance for autonomous robotic ground vehicles. In: P.\u00a0Newman, D.\u00a0Fox, D.\u00a0Hsu (eds.) Robotics: Science and Systems (2013)","key":"344_CR27","DOI":"10.15607\/RSS.2013.IX.014"},{"unstructured":"Modelio web site (2018). http:\/\/www.modelio.org retrieved 11\/29\/2018","key":"344_CR28"},{"unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS. Tech. Rep. NIA 2003-03, NASA\/CR-2003-212418, National Institute of Aerospace, Hampton, VA, USA (2003)","key":"344_CR29"},{"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, June 24, 2013 (2013). https:\/\/doi.org\/10.14279\/tuj.eceasst.69.963.944","key":"344_CR30","DOI":"10.14279\/tuj.eceasst.69.963.944"},{"key":"344_CR31","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., Shankar, N.: PVS: A prototype verification system. In: D.\u00a0Kapur (ed.) Automated Deduction \u2014 CADE-11, Lecture Notes in Computer Science, vol. 607, pp. 748\u2013752. Springer Berlin Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"issue":"2","key":"344_CR32","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S Owre","year":"1995","unstructured":"Owre, S., Rushby, J., Shankar, N., Von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering 21(2), 107\u2013125 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"344_CR33","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-319-74781-1_29","volume-title":"Software Engineering and Formal Methods","author":"Maurizio Palmieri","year":"2018","unstructured":"Palmieri, M., Bernardeschi, C., Masci, P.: Co-simulation of semi-autonomous systems: The line follower robot case study. In: Software Engineering and Formal Methods \u2014 SEFM 2017 Collocated Workshops: DataMod, FAACS, MSE, CoSim-CPS, and FOCLASA, Trento, Italy, September 4-5, 2017, Revised Selected Papers, pp. 423\u2013437 (2017). https:\/\/doi.org\/10.1007\/978-3-319-74781-1_29"},{"key":"344_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-019-00754-9","author":"M Palmieri","year":"2019","unstructured":"Palmieri, M., Bernardeschi, C., Masci, P.: A framework for fmi-based co-simulation of human-machine interfaces. Software and Systems Modeling (2019). https:\/\/doi.org\/10.1007\/s10270-019-00754-9","journal-title":"Software and Systems Modeling"},{"doi-asserted-by":"publisher","unstructured":"Platzer, A., Quesel, J.D.: Keymaera: A hybrid theorem prover for hybrid systems. In: 3rd International Joint Conference on Automated Reasoning (IJCAR), vol. Lecture Notes in Computer Science, pp. 171\u2013178 (2008). https:\/\/doi.org\/10.1109\/ISRCS.2012.6309293","key":"344_CR35","DOI":"10.1109\/ISRCS.2012.6309293"},{"doi-asserted-by":"publisher","unstructured":"Yampolskiy, M., Horvath, P., Koutsoukos, X.D., Xue, Y., Sztipanovits, J.: Systematic analysis of cyber-attacks on cps-evaluating applicability of dfd-based approach. In: 2012 5th International Symposium on Resilient Control Systems, pp. 55\u201362 (2012). https:\/\/doi.org\/10.1109\/ISRCS.2012.6309293","key":"344_CR36","DOI":"10.1109\/ISRCS.2012.6309293"}],"container-title":["Journal of Computer Virology and Hacking Techniques"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11416-019-00344-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11416-019-00344-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11416-019-00344-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T01:07:34Z","timestamp":1610068054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11416-019-00344-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,9]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["344"],"URL":"https:\/\/doi.org\/10.1007\/s11416-019-00344-9","relation":{},"ISSN":["2263-8733"],"issn-type":[{"type":"electronic","value":"2263-8733"}],"subject":[],"published":{"date-parts":[[2020,1,9]]},"assertion":[{"value":"1 August 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 December 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 January 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}