1. Alguliyev, R., Imamverdiyev, Y., Sukhostat, L.: Cyber-physical systems and their security issues. Computers in Industry100, 212–223 (2018).https://doi.org/10.1016/j.compind.2018.04.017

   Article  Google Scholar 

2. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science126(2), 183–235 (1994)

   Article MathSciNet  Google Scholar 

3. 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 Software85(11), 2479–2493 (2012).https://doi.org/10.1016/j.jss.2012.05.061

   Article  Google Scholar 

4. Bagnato, A., Brosse, E., Quadri, I., Sadovykh, A.: INTO-CPS: An integrated “tool chain” 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

5. 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 Systems33(9), 1342–1355 (2014).https://doi.org/10.1109/TCAD.2014.2329419

   Article  Google Scholar 

6. 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–415 (2016).https://doi.org/10.1016/j.ipl.2016.02.001

   Article MathSciNet MATH  Google Scholar 

7. 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–533 (2018).https://doi.org/10.1109/TSE.2017.2694423

   Article  Google Scholar 

8. Blochwitz, T., Otter, M., Akesson, J., Arnold, M., Clauß, 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. 76 in Linköping Electronic Conference Proceedings, pp. 173–184. Linköping University Electronic Press (2012).https://doi.org/10.3384/ecp12076173

9. Broenink, J.F.: 20-SIM software for hierarchical bond-graph/block-diagram models. Simulation Practice and Theory7(5), 481–492 (1999).https://doi.org/10.1016/S0928-4869(99)00018-X

   Article  Google Scholar 

10. Burmester, M., Magkos, E., Chrissikopoulos, V.: Modeling security in cyber-physical systems. International Journal of Critical Infrastructure Protection5(3), 118–126 (2012).https://doi.org/10.1016/j.ijcip.2012.08.002

    Article  Google Scholar 

11. Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.): Methods. Models and Tools for Fault Tolerance. Springer-Verlag, Berlin, Heidelberg (2009)

    MATH  Google Scholar 

12. Dutertre, B.: Elements of mathematical analysis in pvs. In: Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’96, pp. 141–156. Springer-Verlag, Berlin, Heidelberg (1996)

    Google Scholar 

13. Ferrante, A., Kaitovic, I., Milosevic, J.: Modelling requirements for security-enhanced design of embedded systems (2014).https://doi.org/10.5220/0005050003150320

    Article  Google Scholar 

14. Fränzle, M., Herde, C.: Hysat: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design30(3), 179–198 (2007).https://doi.org/10.1007/s10703-006-0031-0

    Article MATH  Google Scholar 

15. Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: Spaceex: Scalable verification of hybrid systems. In: G. Gopalakrishnan, S. Qadeer (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV), no. 6806 in LNCS, pp. 379–395. Springer (2011).https://doi.org/10.1007/978-3-642-22110-1_30

    Chapter  Google Scholar 

16. Humayed, A., Lin, J., Li, F., Luo, B.: Cyber-Physical Systems Security–A Survey. IEEE Internet of Things Journal4(6), 1802–1831 (2017).https://doi.org/10.1109/JIOT.2017.2703172

    Article  Google Scholar 

17. 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. Baier, C. Tinelli (eds.) TACAS,LNCS, vol. 9035, pp. 21–36. Springer (2015).https://doi.org/10.1007/978-3-662-46681-0_2

    Chapter  Google Scholar 

18. Khalil, Y.: A novel probabilistically timed dynamic model for physical security attack scenarios on critical infrastructures. Process Safety and Environmental Protection102, 473–484 (2016).https://doi.org/10.1016/j.psep.2016.05.001

    Article  Google Scholar 

19. 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–315 (2018).https://doi.org/10.1007/978-3-319-98938-9_17

    MATH  Google Scholar 

20. Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The Overture Initiative Integrating Tools for VDM. SIGSOFT Softw. Eng. Notes35(1), 1–6 (2010).https://doi.org/10.1145/1668862.1668864

    Article  Google Scholar 

21. 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–6 (2016).https://doi.org/10.1109/CPSData.2016.7496424

22. Masci, P., Zhang, Y., Jones, P.L., Oladimeji, P., D’Urso, 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–214 (2014).https://doi.org/10.1007/978-3-319-06200-6_16

    Google Scholar 

23. Mauro, G., Thimbleby, H., Domenici, A., Bernardeschi, C.: Extending a user interface prototyping tool with automatic MISRA C code generation. In: C. Dubois, P. Masci, D. Méry (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–66. Open Publishing Association, (2017).https://doi.org/10.4204/EPTCS.240.4

    Article  Google Scholar 

24. Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE Journal on Selected Areas in Communications21(1), 44–54 (2003).https://doi.org/10.1109/JSAC.2002.806125

    Article  Google Scholar 

25. Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.: Hey malware, i can find you! pp. 261–262 (2016).https://doi.org/10.1109/WETICE.2016.67

26. Mitchell, R., Chen, I.: Modeling and analysis of attacks and counter defense mechanisms for cyber physical systems. IEEE Transactions on Reliability65(1), 350–358 (2016).https://doi.org/10.1109/TR.2015.2406860

    Article  Google Scholar 

27. Mitsch, S., Ghorbal, K., Platzer, A.: On provably safe obstacle avoidance for autonomous robotic ground vehicles. In: P. Newman, D. Fox, D. Hsu (eds.) Robotics: Science and Systems (2013)

28. Modelio web site (2018).http://www.modelio.org retrieved 11/29/2018

29. Muñoz, C.: Rapid prototyping in PVS. Tech. Rep. NIA 2003-03, NASA/CR-2003-212418, National Institute of Aerospace, Hampton, VA, USA (2003)

30. 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

31. Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: D. Kapur (ed.) Automated Deduction — CADE-11,Lecture Notes in Computer Science, vol. 607, pp. 748–752. Springer Berlin Heidelberg (1992).https://doi.org/10.1007/3-540-55602-8_217

    Chapter  Google Scholar 

32. 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 Engineering21(2), 107–125 (1995)

    Article  Google Scholar 

33. Palmieri, M., Bernardeschi, C., Masci, P.: Co-simulation of semi-autonomous systems: The line follower robot case study. In: Software Engineering and Formal Methods — SEFM 2017 Collocated Workshops: DataMod, FAACS, MSE, CoSim-CPS, and FOCLASA, Trento, Italy, September 4-5, 2017, Revised Selected Papers, pp. 423–437 (2017).https://doi.org/10.1007/978-3-319-74781-1_29

    Chapter  Google Scholar 

34. 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

    Article  Google Scholar 

35. 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–178 (2008).https://doi.org/10.1109/ISRCS.2012.6309293

36. 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–62 (2012).https://doi.org/10.1109/ISRCS.2012.6309293

Download references