Advertisement

A Calculus of Cyber-Physical Systems

  • Ruggero LanotteEmail author
  • Massimo Merro
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10168)

Abstract

We propose a hybrid process calculus for modelling and reasoning on cyber-physical systems (CPSs). The dynamics of the calculus is expressed in terms of a labelled transition system in the SOS style of Plotkin. This is used to define a bisimulation-based behavioural semantics which support compositional reasonings. Finally, we prove run-time properties and system equalities for a non-trivial case study.

Keywords

Process calculus Cyber-physical system Semantics 

Notes

Acknowledgements

We thank Riccardo Muradore for providing us with simulations in MATLAB of our case study. We thank the anonymous reviewers for valuable comments.

References

  1. 1.
    Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). doi: 10.1007/3-540-57318-6_30 CrossRefGoogle Scholar
  2. 2.
    Bergstra, J.A., Middleburg, C.A.: Process algebra for hybrid systems. TCS 335(2–3), 215–280 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bodei, C., Degano, P., Ferrari, G.-L., Galletta, L.: Where do your iot ingredients come from? In: Lluch Lafuente, A., Proença, J. (eds.) COORDINATION 2016. LNCS, vol. 9686, pp. 35–50. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-39519-7_3 Google Scholar
  4. 4.
    Cerone, A., Hennessy, M., Merro, M.: Modelling MAC-layer communications in wireless systems. Logical Meth. Comput. Sci. 11(1:18), 1–59 (2015)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Cuijpers, P., Reniers, M.: Hybrid process algebra. JLAP 62(2), 191–245 (2005)MathSciNetzbMATHGoogle Scholar
  6. 6.
    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22110-1_27 CrossRefGoogle Scholar
  7. 7.
    Galpin, V., Bortolussi, L., Hillston, J.: HYPE: hybrid modelling by composition of flows. Formal Aspects Comput. 25(4), 503–541 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Hennessy, M., Regan, T.: A process algebra for timed systems. I&C 117(2), 221–239 (1995)MathSciNetzbMATHGoogle Scholar
  9. 9.
    Lanese, I., Bedogni, L., Di Felice, M.: Internet of things: a process calculus approach. In: Shin, S., Maldonado, J. (eds.) ACM SAC 2013, pp. 1339–1346. ACM (2013)Google Scholar
  10. 10.
    Lanotte, R., Merro, M.: A calculus of cyber-physical systems. CoRR abs/1612.00484 (2016)Google Scholar
  11. 11.
    Lanotte, R., Merro, M.: A semantic theory of the internet of things. In: Lluch Lafuente, A., Proença, J. (eds.) COORDINATION 2016. LNCS, vol. 9686, pp. 157–174. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-39519-7_10 Google Scholar
  12. 12.
    Lanotte, R., Merro, M., Muradore, R., Viganò, L.: A formal approach to cyber-physical attacks. CoRR abs/1611.01377 (2016)Google Scholar
  13. 13.
    Merro, M., Ballardin, F., Sibilio, E.: A timed calculus for wireless systems. TCS 412(47), 6585–6611 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of real-time maude. High.-Order Symb. Comput. 20(1–2), 161–196 (2007)CrossRefzbMATHGoogle Scholar
  15. 15.
    Rounds, W.C., Song, H.: The \(\phi \)-calculus: a language for distributed control of reconfigurable embedded systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 435–449. Springer, Heidelberg (2003). doi: 10.1007/3-540-36580-X_32 CrossRefGoogle Scholar
  16. 16.
    Vigo, R., Nielson, F., Nielson, H.R.: Broadcast, denial-of-service, and secure communication. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 412–427. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38613-8_28 CrossRefGoogle Scholar
  17. 17.
    Zacchia Lun, Y., D’Innocenzo, A., Malavolta, I., Di Benedetto, M.D.: Cyber-physical systems security: a systematic mapping study. CoRR abs/1605.09641 (2016)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Dipartimento di Scienza e Alta TecnologiaUniversità dell’InsubriaComoItaly
  2. 2.Dipartimento di InformaticaUniversità degli Studi di VeronaVeronaItaly

Personalised recommendations