Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This work has been partially supported by the LabEx PERSYVAL-Lab (ANR-11-LABX-0025-01).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    TargetLink is a production code generation tool from dSPACE.

  2. 2.

    more commonly called Assume/Guarantee reasoning, but we adopt here the terminology of [11].

  3. 3.

    where it may be necessary to “translate” the viewpoint property to a system property, but this requires technical arguments which beyond the purpose of this paper.

  4. 4.

    Note that sometimes it may be sufficient to relax the notion of abstraction to obtain a conditional abstraction.

References

  1. aiT. https://www.absint.com/ait/

  2. RT-Druid. http://www.evidence.eu.com/products/rt-druid.html

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

    Chapter  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

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

    Article  Google Scholar 

  9. Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Software 28(3), 41–48 (2011)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  11. Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Design Autom. 12(2–3), 124–400 (2018)

    Article  Google Scholar 

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

    Chapter  Google Scholar 

  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. 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. 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. Fontanelli, D., Greco, L., Palopoli, L.: Soft real-time scheduling for embedded control systems. Automatica 49(8), 2330–2338 (2013)

    Article  MathSciNet  Google Scholar 

  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_17

    Chapter  MATH  Google Scholar 

  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. Gärtner, F.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Comput. Surv. 31(1), 1–26 (1999)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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_8

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  30. Meyer, B.: Applying “design by contract”. IEEE Computer 25(10), 40–51 (1992)

    Article  Google Scholar 

  31. Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)

    Article  MathSciNet  Google Scholar 

  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_8

    Chapter  Google Scholar 

  33. Otter, M., Mattsson, S., Elmqvist, H.: Multidomain modeling with Modelica. In: Handbook of Dynamic System Modeling. Chapmanand Hall/CRC (2007)

    Google Scholar 

  34. Passerone, R., et al.: Metamodels in Europe: languages, tools, and applications. IEEE Des. Test Comput. 26(3) (2009)

    Google Scholar 

  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)

    Article  Google Scholar 

  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_5

    Chapter  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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/BFb0023444

    Chapter  Google Scholar 

  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-5

    Book  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    MATH  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, Grenoble, France

    Susanne Graf

  2. Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, Grenoble, France

    Sophie Quinton, Alain Girault & Gregor Gössler

Authors
  1. Susanne Graf
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sophie Quinton
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alain Girault
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gregor Gössler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Susanne Graf .

Editor information

Editors and Affiliations

  1. Technical University of Dortmund, Dortmund, Germany

    Falk Howar

  2. Masaryk University, Brno, Czech Republic

    Jiří Barnat

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Graf, S., Quinton, S., Girault, A., Gössler, G. (2018). Building Correct Cyber-Physical Systems: Why We Need a Multiview Contract Theory. In: Howar, F., Barnat, J. (eds) Formal Methods for Industrial Critical Systems. FMICS 2018. Lecture Notes in Computer Science(), vol 11119. Springer, Cham. https://doi.org/10.1007/978-3-030-00244-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-00244-2_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-00243-5

  • Online ISBN: 978-3-030-00244-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation