Advertisement

Building Correct Cyber-Physical Systems: Why We Need a Multiview Contract Theory

  • Susanne Graf
  • Sophie Quinton
  • Alain Girault
  • Gregor Gössler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11119)

Abstract

The design and verification of critical cyber-physical systems is based on a number of models (and corresponding analysis techniques and tools) representing different viewpoints such as function, timing, security and many more. Overall correctness is guaranteed by mostly informal, and therefore basic, arguments about the relationship between these viewpoint-specific models. We believe that a more flexible contract-based approach could lead to easier integration, to relaxed assumptions, and consequently to more cost efficient systems while preserving the current modelling approach and its tools.

References

  1. 1.
  2. 2.
  3. 3.
    Al Khatib, M., Girard, A., Dang, T.: Scheduling of embedded controllers under timing contracts. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017. ACM, New York (2017)Google Scholar
  4. 4.
    Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45657-0_30CrossRefzbMATHGoogle Scholar
  5. 5.
    Assayad, I., Girault, A., Kalla, H.: Tradeoff exploration between reliability, power consumption, and execution time for embedded systems. Int. J. Software Tools Technol. Transfer 15(3), 229–243 (2013)CrossRefGoogle Scholar
  6. 6.
    Avizienis, A., Laprie, J.-C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secure Comput. 1(1), 11–33 (2004)CrossRefGoogle Scholar
  7. 7.
    Axer, P., Ernst, R.: Stochastic response-time guarantee for non-preemptive, fixed-priority scheduling under errors. In: The 50th Annual Design Automation Conference 2013, DAC 2013, Austin, TX, USA, 29 May–07 June 2013. ACM (2013)Google Scholar
  8. 8.
    Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A.: Metropolis: an integrated electronic system design environment. Computer 36(4), 45–52 (2003)CrossRefGoogle Scholar
  9. 9.
    Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Software 28(3), 41–48 (2011)CrossRefGoogle Scholar
  10. 10.
    Benveniste, A., Caillaud, B., Carloni, L.P., Caspi, P., Sangiovanni-Vincentelli, A.L.: Composing heterogeneous reactive systems. ACM Trans. Embedded Comput. Syst. 7(4), 43 (2008)CrossRefGoogle Scholar
  11. 11.
    Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Design Autom. 12(2–3), 124–400 (2018)CrossRefGoogle Scholar
  12. 12.
    Bhat, A., Samii, S., Rajkumar, R.R.: Recovery time considerations in real-time systems employing software fault tolerance. In: Altmeyer, S. (ed.) 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), vol. 106. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)Google Scholar
  13. 13.
    Brière, D., Ribot, D., Pilaud, D., Camus, J.-L.: Methods and specifications tools for Airbus on-board systems. In: Avionics Conference and Exhibition, London, UK. ERA Technology (1994)Google Scholar
  14. 14.
    Damm, W., Dierks, H., Oehlerking, J., Pnueli, A.: Towards component based design of hybrid systems: safety and stability. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 96–143. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-13754-9_6CrossRefGoogle Scholar
  15. 15.
    Derler, P., Lee, E., Tripakis, S., Törngren, M.: Cyber-physical system design contracts. In: Proceedings of the ACM/IEEE 4th International Conference on Cyber-Physical Systems, ICCPS 2013. ACM, New York (2013)Google Scholar
  16. 16.
    Ernst, R., Henia, R., Quinton, S.: Beyond the deadline: new interfaces between control and scheduling for the design and analysis of critical embedded systems. Tutorial at ESWeek (2017)Google Scholar
  17. 17.
    Fellmuth, J., Göthel, T., Glesner, S.: Instruction caches in static WCET analysis of artificially diversified software. In: Altmeyer, S. (ed.) 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), vol. 106. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)Google Scholar
  18. 18.
    Fontanelli, D., Greco, L., Palopoli, L.: Soft real-time scheduling for embedded control systems. Automatica 49(8), 2330–2338 (2013)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31954-2_17CrossRefzbMATHGoogle Scholar
  20. 20.
    Frehse, G., Hamann, A., Quinton, S., Woehrle, M.: Formal analysis of timing effects on closed-loop properties of control software. In: Proceedings of the IEEE 35th IEEE Real-Time Systems Symposium, RTSS 2014, Rome, Italy, 2–5 December 2014. IEEE Computer Society (2014)Google Scholar
  21. 21.
    Gärtner, F.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Comput. Surv. 31(1), 1–26 (1999)CrossRefGoogle Scholar
  22. 22.
    Girault, A., Kalla, H.: A novel bicriteria scheduling heuristics providing a guaranteed global system failure rate. IEEE Trans. Dependable Secure Comput. 6(4), 241–254 (2009)CrossRefGoogle Scholar
  23. 23.
    Graf, S., Passerone, R., Quinton, S.: Contract-based reasoning for component systems with rich interactions. In: Sangiovanni-Vincentelli, A.L., Zeng, H., Natale, M.D., Marwedel, P. (eds.) Embedded Systems Development: From Functional Models to Implementations. Springer, New York (2014).  https://doi.org/10.1007/978-1-4614-3879-3_8CrossRefGoogle Scholar
  24. 24.
    Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) Computer-Aided Verification, Proceedings of a DIMACS Workshop 1990, New Brunswick, New Jersey, USA, 18–21 June 1990, vol. 3. DIMACS Series in Discrete Mathematics and Theoretical Computer Science (1990)Google Scholar
  25. 25.
    Henia, R., Hamann, A., Jersak, M., Racu, R., Richter, K., Ernst, R.: System level performance analysis–the symta/s approach. In: IEE Proceedings - Computers and Digital Techniques, vol. 152 (2005)Google Scholar
  26. 26.
    Krüger, K., Völp, M., Fohler, G.: Vulnerability analysis and mitigation of directed timing inference based attacks on time-triggered systems. In: Altmeyer, S. (ed.) 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), vol. 106. Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)Google Scholar
  27. 27.
    Kumar, P., Goswami, D., Chakraborty, S., Annaswamy, A., Lampka, K., Thiele, L.: A hybrid approach to cyber-physical systems verification. In: Proceedings of the 49th Annual Design Automation Conference, DAC 2012. ACM (2012)Google Scholar
  28. 28.
    Li, J., Nuzzo, P., Sangiovanni-Vincentelli, A., Xi, Y., Li, D.: Stochastic contracts for cyber-physical system design under probabilistic requirements. In: Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, New York, NY, USA. ACM (2017)Google Scholar
  29. 29.
    Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Design 6(1), 11–44 (1995)CrossRefGoogle Scholar
  30. 30.
    Meyer, B.: Applying “design by contract”. IEEE Computer 25(10), 40–51 (1992)CrossRefGoogle Scholar
  31. 31.
    Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Müller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: Change and delay contracts for hybrid system component verification. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 134–151. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54494-5_8CrossRefGoogle Scholar
  33. 33.
    Otter, M., Mattsson, S., Elmqvist, H.: Multidomain modeling with Modelica. In: Handbook of Dynamic System Modeling. Chapmanand Hall/CRC (2007)Google Scholar
  34. 34.
    Passerone, R., et al.: Metamodels in Europe: languages, tools, and applications. IEEE Des. Test Comput. 26(3) (2009)Google Scholar
  35. 35.
    Castaneda, G.A.P., Aubry, J.-F., Brinzei, N.: Stochastic hybrid automata model for dynamic reliability assessment. Proc. Inst. Mech. Eng. Part O J. Risk Reliab. 225(1), 28–41 (2011)CrossRefGoogle Scholar
  36. 36.
    Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 13. Springer, Heidelberg (1985).  https://doi.org/10.1007/978-3-642-82453-1_5CrossRefzbMATHGoogle Scholar
  37. 37.
    Powell, D.: Failure mode assumption and assumption coverage. In: International Symposium on Fault-Tolerant Computing, FTCS-22, Boston, MA, USA. IEEE. Research report LAAS 91462 (1992)Google Scholar
  38. 38.
    Reineke, J., Tripakis, S.: Basic problems in multi-view modeling. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 217–232. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54862-8_15CrossRefGoogle Scholar
  39. 39.
    Sheikh, H., Ahmad, I.: Sixteen heuristics for joint optimization of performance, energy, and temperature in allocating tasks to multi-cores. ACM Trans. Parallel Comput. 3(2), 9 (2016)MathSciNetCrossRefGoogle Scholar
  40. 40.
    Steffen, B.: Unifying models. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 1–20. Springer, Heidelberg (1997).  https://doi.org/10.1007/BFb0023444CrossRefGoogle Scholar
  41. 41.
    Tabuada, P.: Verification and Control of Hybrid Systems - A Symbolic Approach. Springer, New York (2009).  https://doi.org/10.1007/978-1-4419-0224-5CrossRefzbMATHGoogle Scholar
  42. 42.
    Theiling, H., Ferdinand, C., Wilhelm, R.: Fast and precise WCET prediction by separated cache and path analyses. Real-Time Syst. 18(2/3), 157–179 (2000)CrossRefGoogle Scholar
  43. 43.
    Zhao, Y., Xiong, Y., Lee, E.A., Liu, X., Zhong, L.C.: The design and application of structured types in ptolemy II. Int. J. Intell. Syst. 25(2), 118–136 (2010)zbMATHGoogle Scholar
  44. 44.
    Zhu, D., Melhem, R., Mossé, D.: The effects of energy management on reliability in real-time embedded systems. In: International Conference on Computer Aided Design, ICCAD 2004, San Jose, CA, USA (2004)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Susanne Graf
    • 1
  • Sophie Quinton
    • 2
  • Alain Girault
    • 2
  • Gregor Gössler
    • 2
  1. 1.Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAGGrenobleFrance
  2. 2.Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIGGrenobleFrance

Personalised recommendations