[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

From Interface Automata to Hypercontracts

  • Chapter
  • First Online:
Principles of Systems Design

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13660))

Abstract

de Alfaro and Henzinger’s interface automata brought renewed vigor to the tasks of specifying software formally and reasoning about systems compositionally. The key ingredients to this approach were the separation of concerns between environment and implementation, a light-weight behavioral interface that enabled more comprehensive compatibility checks than those allowed by type checking, and the notion of optimistic composition of specifications. This new impetus helped launch a research program of formally analyzing and designing general cyber-physical systems compositionally, where contract-based design has been playing a fundamental role. In this paper, we discuss the path connecting interface automata to the theory of contracts, with a special emphasis on hypercontracts, a recent development of contract theory.

This paper is based on [20] and [22].

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 63.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 79.99
Price includes VAT (United Kingdom)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    To simplify our development, we assume that all interface automata share the same action alphabet.

  2. 2.

    Since the sets of input and output actions for a given IA partition \(\varSigma \), this condition is equivalent to requiring that the two IA don’t share outputs.

References

  1. Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993)

    Article  Google Scholar 

  2. de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the 8th European Software Engineering Conference Held Jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 109–120 ESEC/FSE-9, Association for Computing Machinery, New York, NY, USA (2001)

    Google Scholar 

  3. de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Timed interfaces. In: Sangiovanni-Vincentelli, A., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 108–122. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45828-X_9

    Chapter  Google Scholar 

  4. Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055622

    Chapter  Google Scholar 

  5. Bartocci, E., Ferrère, T., Henzinger, T.A., Nickovic, D., Da Costa, A.O.: Information-flow interfaces. In: Johnsen, E.B., Wimmer, M. (eds.) Fundamental Approaches to Software Engineering. FASE 2022. LNCS, vol. 13241, pp. 3–22. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99429-7

  6. Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200–225. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92188-2_9

    Chapter  MATH  Google Scholar 

  7. Benveniste, A., et al.: Contracts for system design. Foundations and Trends® in Electronic Design Automation, vol. 12(2–3), pp. 124–400 (2018)

    Google Scholar 

  8. Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource Interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117–133. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45212-6_9

    Chapter  Google Scholar 

  9. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774

    Chapter  Google Scholar 

  10. Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)

    Article  Google Scholar 

  11. Damm, W.: Controlling speculative design processes using rich component models. In: Fifth International Conference on Application of Concurrency to System Design (ACSD2005), pp. 118–119 (2005)

    Google Scholar 

  12. David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 91–100. HSCC 2010, Association for Computing Machinery, New York, NY, USA (2010)

    Google Scholar 

  13. Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)

    Google Scholar 

  14. Doyen, L., Henzinger, T.A., Jobstmann, B., Petrov, T.: Interface theories with component reuse. In: Proceedings of the 8th ACM International Conference on Embedded Software, pp. 79–88 EMSOFT 2008, Association for Computing Machinery, New York, NY, USA (2008)

    Google Scholar 

  15. Floyd, R.W.: Assigning meanings to programs. Proceed. Symp. Appl. Math. 19, 19–32 (1967)

    Article  MathSciNet  MATH  Google Scholar 

  16. Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy. Oakland, CA, USA, April 26–28, 1982, pp. 11–20 IEEE Computer Society, Oakland, CA, USA (1982)

    Google Scholar 

  17. Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series, vol. 13, pp. 477–498. Springer, Heidelberg (1985). https://doi.org/10.1007/978-3-642-82453-1_17

  18. Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive interfaces. SIGSOFT Softw. Eng. Notes 30(5), 31–40 (2005)

    Google Scholar 

  19. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  20. Incer, I.: The algebra of contracts, Ph. D. thesis, EECS Department, University of California, Berkeley (2022)

    Google Scholar 

  21. Incer, I., Benveniste, A., Sangiovanni-Vincentelli, A., Seshia, S.A.: Hypercontracts. arXiv preprint arXiv:2106.02449 (2021)

  22. Incer, I., Benveniste, A., Sangiovanni-Vincentelli, A., Seshia, S.A.: Hypercontracts. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods, pp. 674–692. Springer International Publishing, Cham (2022)

    Chapter  Google Scholar 

  23. Lamport, L.: The computer science of concurrency: the early years. Commun. ACM 58(6), 71–76 (2015)

    Google Scholar 

  24. Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_6

    Chapter  MATH  Google Scholar 

  25. Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2, 219–246 (1989)

    MathSciNet  MATH  Google Scholar 

  26. Mastroeni, I., Pasqua, M.: Verifying bounded subset-closed hyperproperties. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 263–283. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99725-4_17

    Chapter  Google Scholar 

  27. Negulescu, R.: Process spacess. Tech. Rep. CS-95-48, University of Waterloo (1995)

    Google Scholar 

  28. Parnas, D.L.: A technique for software module specification with examples. Commun. ACM 15(5), 330–336 (1972)

    Google Scholar 

  29. Passerone, R., Incer, I., Sangiovanni-Vincentelli, A.L.: Coherent extension, composition, and merging operators in contract models for system design. ACM Trans. Embed. Comput. Syst. 18(5s), 1–23 (2019)

    Google Scholar 

  30. Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977)(FOCS), pp. 46–57 (1977)

    Google Scholar 

  31. Rabe, M.N.: A temporal logic approach to information-flow control, Ph. D. thesis, Universität des Saarlandes (2016)

    Google Scholar 

  32. Raclet, J.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93–110 (2008)

    Article  Google Scholar 

  33. Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fund. Inform. 108(1–2), 119–149 (2011)

    MathSciNet  MATH  Google Scholar 

  34. Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217–238 (2012)

    Google Scholar 

  35. Sifakis, J.: Rigorous system design. Foundations and Trends® in Electronic Design Automation, vol. 6, no. 4, pp. 293–362 (2013)

    Google Scholar 

  36. Turing, A.M.: On checking a large routine. In: Report of a Conference on High-Speed Automatic Calculating Machines, pp. 67–69. University Mathematical Laboratory, Cambridge (1949)

    Google Scholar 

Download references

Acknowledgments

This work was supported by NSF Contract CPS Medium 1739816, by the DARPA LOGiCS project under contract FA8750-20-C-0156, and by the Chateaubriand Fellowship of the Office for Science & Technology of the Embassy of France in the United States.

Author information

Authors and Affiliations

  1. University of California, Berkeley, USA

    Inigo Incer, Alberto Sangiovanni-Vincentelli & Sanjit A. Seshia

  2. INRIA/IRISA, Rennes, France

    Inigo Incer & Albert Benveniste

Authors
  1. Inigo Incer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Albert Benveniste
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alberto Sangiovanni-Vincentelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sanjit A. Seshia
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Inigo Incer .

Editor information

Editors and Affiliations

  1. Université Libre de Bruxelles, Brussels, Belgium

    Jean-François Raskin

  2. Institute of Science and Technology Austria, Klosterneuburg, Austria

    Krishnendu Chatterjee

  3. École Normale Supérieure Paris-Saclay, Gif-sur-Yvette, France

    Laurent Doyen

  4. MPI for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Incer, I., Benveniste, A., Sangiovanni-Vincentelli, A., Seshia, S.A. (2022). From Interface Automata to Hypercontracts. In: Raskin, JF., Chatterjee, K., Doyen, L., Majumdar, R. (eds) Principles of Systems Design. Lecture Notes in Computer Science, vol 13660. Springer, Cham. https://doi.org/10.1007/978-3-031-22337-2_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-22337-2_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-22336-5

  • Online ISBN: 978-3-031-22337-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation