Skip to main content
SpringerLink
Log in

Hierarchical System Design with Vertical Contracts

  • Chapter
  • First Online:
Book cover Principles of Modeling

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10760))

Abstract

We propose the notions of heterogeneous refinement and vertical contracts as additions for any contract framework to provide full methodological support for multi-view and multi-layer system design with heterogeneous models. We rethink the relation of contract refinement in the context of layered design and discuss how it can be extended, via heterogeneous refinement and vertical contracts, to deal with hierarchies of models that present heterogeneous architectures as well as behaviors expressed by heterogeneous formalisms. We then show via design examples that such an extension can, indeed, encompass a richer set of design refinement relations, including support for synthesis methods and optimized mappings of specifications into implementations.

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.

    A more general definition of component distinguishes between variables and ports [36]. For simplicity, in this paper, we use the same term variables to denote both component variables and ports.

  2. 2.

    We also use the fact that \(\mathcal {M}^{-1}(\overline{A'}) = \overline{\mathcal {M}^{-1}(A')}\) for any subset \(A'\) of the universal set \(B'\). In fact, we have \(B = \mathcal {M}^{-1}(B') = \mathcal {M}^{-1}(A' \cup \overline{A'}) = \mathcal {M}^{-1}(A') \cup \mathcal {M}^{-1}(\overline{A'})\), \(\emptyset = \mathcal {M}^{-1}(A'\cap \overline{A'}) = \mathcal {M}^{-1}(A') \cap \mathcal {M}^{-1}(\overline{A'})\), which jointly lead to \(\mathcal {M}^{-1}(\overline{A'}) = \overline{\mathcal {M}^{-1}(A')}\).

  3. 3.

    We are actually interested in checking consistency \(\forall t_{on}: t_{on} \le (t_d-\varDelta )\), which is the set of legal environments for \(\tilde{\mathcal {C}}^t\). In fact, we want to show that, for each \(t_{on}\) satisfying the assumptions of the specification contract \(\tilde{\mathcal {C}}^t\), there exists an implementable \(t_{pow}\), according to the implementation contract \(\tilde{\mathcal {M}}^t\), which also satisfies the deadline \(t_d\), as required by \(\tilde{\mathcal {C}}^t\). When \(t_{on} > (t_d-\varDelta )\), \(\tilde{\mathcal {C}}^t \wedge \tilde{\mathcal {M}}^t\) is trivially consistent, since the guarantees of \(\tilde{\mathcal {C}}^t\) are vacuously true.

  4. 4.

    We observe that the structural decomposition adopted in (4) is just an example. Another alternative could be to represent the left-hand side contract as \(\bigotimes _{i=1}^n (\mathcal {C}_{Hi}^{l} \wedge \mathcal {C}_{Ti}^{l})\).

  5. 5.

    For simplicity, we drop the symbol of the architecture mapping \(\mathcal {V}\) from the expressions of the vertical contracts in this section and in the following ones.

References

  1. de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings of the Symposium Foundations of Software Engineering, pp. 109–120. ACM Press (2001)

    Google Scholar 

  2. de Alfaro, L., Henzinger, T.A.: Interface theories for component-based design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 148–165. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45449-7_11

    Chapter  Google Scholar 

  3. Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)

    Article  Google Scholar 

  4. Alur, R., Dang, T., Ivančić, F.: Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2), 250–271 (2006)

    Article  MathSciNet  Google Scholar 

  5. Balarin, F., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A.L., Watanabe, Y.: Metropolis: an integrated electronic system design environment. Computer 36(4), 45–52 (2003)

    Article  Google Scholar 

  6. Balarin, F., Davare, A., D’Angelo, M., Densmore, D., Meyerowitz, T., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A., Simalatsar, A., Watanabe, Y., Yang, G., Zhu, Q.: Platform-based design and frameworks: metropolis and metro II. In: Nicolescu, G., Mosterman, P.J. (eds.) Model-Based Design for Embedded Systems, Chap. 10, p. 259. CRC Press, Taylor and Francis Group, Boca Raton, London, New York, November 2009

    Chapter  Google Scholar 

  7. Benveniste, A., et al.: 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  Google Scholar 

  8. Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K.G.: Contracts for System Design. Rapport de recherche RR-8147, INRIA, November 2012

    Google Scholar 

  9. Benveniste, A., Nickovic, D., Henzinger, T.: Compositional contract abstraction for system design. Research Report RR-8460, INRIA, January 2014

    Google Scholar 

  10. Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA\(^{+}\) proof system: building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, p. 44. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14808-8_3. http://dl.acm.org/citation.cfm?id=1881833.1881837

    Chapter  Google Scholar 

  11. Chutinan, A., Krogh, B.: Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Trans. Autom. Control 46(9), 1401–1410 (2001)

    Article  MathSciNet  Google Scholar 

  12. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2008)

    Google Scholar 

  13. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symposium on Principles of Programming Languages (POPL), pp. 238–252. ACM Press (1977)

    Google Scholar 

  14. Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: Proceedings of the Hybrid Systems: Computation and Controlm, HSCC 2010, pp. 11–20. ACM, New York (2010). https://doi.org/10.1145/1755952.1755956

  15. Derler, P., Lee, E.A., Tripakis, S., Törngren, M.: Cyber-physical system design contracts. In: Proceedings of the International Conference Cyber-Physical Systems, pp. 109–118 (2013). https://doi.org/10.1145/2502524.2502540

  16. Finn, J., Nuzzo, P., Sangiovanni-Vincentelli, A.: A mixed discrete-continuous optimization scheme for cyber-physical system architecture exploration. In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, pp. 216–223, November 2015

    Google Scholar 

  17. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transfer 10, 263–279 (2008)

    Article  Google Scholar 

  18. Garcia, C.E., Prett, D.M., Morari, M.: Model predictive control: theory and practice – a survey. Automatica 25(3), 335–348 (1989). http://www.sciencedirect.com/science/article/pii/0005109889900022

    Article  Google Scholar 

  19. Guo, L., Zhu, Q., Nuzzo, P., Passerone, R., Sangiovanni-Vincentelli, A., Lee, E.A.: Metronomy: a function-architecture co-simulation framework for timing verification of cyber-physical systems. In: Proceedings of the International Conference Hardware-Software Codesign and System Synthesis, pp. 24:1–24:10, October 2014

    Google Scholar 

  20. Henzinger, T., Ho, P.H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43(4), 540–554 (1998)

    Article  MathSciNet  Google Scholar 

  21. Jin, B., Nuzzo, P., Maasoumy, M., Zhou, Y., Sangiovanni-Vincentelli, A.: A contract-based framework for integrated demand response management in smart grids. In: Proceedings of the International Conference Embedded Systems for Energy-Efficient Built Environments, pp. 167–176. ACM (2015)

    Google Scholar 

  22. Keutzer, K., Malik, S., Newton, R., Rabaey, J., Sangiovanni Vincentelli, A.: System level design: orthogonalization of concerns and platform-based design. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 19(12), 1523–1543 (2000)

    Article  Google Scholar 

  23. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  24. Lee, E.A., Sangiovanni-Vincentelli, A.: A framework for comparing models of computation. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 17(12), 1217–1229 (1998)

    Article  Google Scholar 

  25. Leung, M.-K., et al.: Scalable semantic annotation using lattice-based ontologies. In: Schürr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 393–407. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04425-0_31

    Chapter  Google Scholar 

  26. 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 International Conference Formal Methods and Models for Co-design, September 2017

    Google Scholar 

  27. Lohstroh, M., Lee, E.A.: An interface theory for the internet of things. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 20–34. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_2

    Chapter  Google Scholar 

  28. Maasoumy, M., Nuzzo, P., Sangiovanni-Vincentelli, A.: Smart buildings in the smart grid: contract-based design of an integrated energy management system. In: Khaitan, S.K., McCalley, J.D., Liu, C.C. (eds.) Cyber Physical Systems Approach to Smart Electric Power Grid. PS, pp. 103–132. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-45928-7_5

    Chapter  Google Scholar 

  29. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12

    Chapter  MATH  Google Scholar 

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

    Article  Google Scholar 

  31. Nuzzo, P., Finn, J.B., Iannopollo, A., Sangiovanni-Vincentelli, A.L.: Contract-based design of control protocols for safety-critical cyber-physical systems. In: Proceedings of the Design, Automation and Test in Europe Conference, pp. 1–4, March 2014

    Google Scholar 

  32. Nuzzo, P., Iannopollo, A., Tripakis, S., Sangiovanni-Vincentelli, A.L.: Are interface theories equivalent to contract theories? In: International Conference on Formal Methods and Models for Co-design, pp. 104–113, October 2014

    Google Scholar 

  33. Nuzzo, P., Sangiovanni-Vincentelli, A., Sun, X., Puggelli, A.: Methodology for the design of analog integrated interfaces using contracts. IEEE Sens. J. 12(12), 3329–3345 (2012)

    Article  Google Scholar 

  34. Nuzzo, P., Sangiovanni-Vincentelli, A.L., Murray, R.M.: Methodology and tools for next generation cyber-physical systems: the iCyPhy approach. In: Proceedings of the INCOSE International Symposium, vol. 25, pp. 235–249. Wiley Online Library, July 2015

    Article  Google Scholar 

  35. Nuzzo, P., Xu, H., Ozay, N., Finn, J., Sangiovanni-Vincentelli, A., Murray, R., Donzé, A., Seshia, S.: A contract-based methodology for aircraft electric power system design. IEEE Access 2, 1–25 (2014)

    Article  Google Scholar 

  36. Nuzzo, P.: Compositional design of cyber-physical systems using contracts. Ph.D. thesis, EECS Department, University of California, Berkeley, August 2015. http://www.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-189.html

  37. Nuzzo, P., Lora, M., Feldman, Y., Sangiovanni-Vincentelli, A.: CHASE: contract-based requirement engineering for cyber-physical system design. In: Proceedings of the Design, Automation and Test in Europe Conference Dresden, Germany (2018, to appear)

    Google Scholar 

  38. Nuzzo, P., Sangiovanni-Vincentelli, A.: System design in the cyber-physical era. In: Nanoelectronics: Materials, Devices, Applications, pp. 363–396 (2017). https://doi.org/10.1002/9783527800728.ch15

    Chapter  Google Scholar 

  39. Nuzzo, P., Sangiovanni-Vincentelli, A.: Robustness in analog systems: design techniques, methodologies and tools. In: Proceedings of the IEEE Symposium Industrial Embedded Systems, pp. 194–203, June 2011

    Google Scholar 

  40. Nuzzo, P., Sangiovanni-Vincentelli, A.: Let’s get physical: computer science meets systems. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) ETAPS 2014. LNCS, vol. 8415, pp. 193–208. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54848-2_13

    Chapter  MATH  Google Scholar 

  41. Nuzzo, P., Sangiovanni-Vincentelli, A., Bresolin, D., Geretti, L., Villa, T.: A platform-based design methodology with contracts and related tools for the design of cyber-physical systems. Proc. IEEE 103(11), 2104–2132 (2015)

    Article  Google Scholar 

  42. Passerone, R., Burch, J.R., Sangiovanni-Vincentelli, A.L.: Refinement preserving approximations for the design and verification of heterogeneous systems. Formal Methods Syst. Des. 31(1), 1–33 (2007). https://doi.org/10.1007/s10703-006-0024-z

    Article  MATH  Google Scholar 

  43. Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_24

    Chapter  Google Scholar 

  44. Pnueli, A.: The temporal logic of programs. In: Symposium Foundations of Computer Science, vol. 31, pp. 46–57, November 1977

    Google Scholar 

  45. Rajhans, A., Bhave, A., Ruchkin, I., Krogh, B.H., Garlan, D., Platzer, A., Schmerl, B.: Supporting heterogeneity in cyber-physical systems architectures. IEEE Trans. Autom. Control 59(12), 3178–3193 (2014)

    Article  MathSciNet  Google Scholar 

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

  47. Sangiovanni-Vincentelli, A.: Quo vadis, SLD? Reasoning about the trends and challenges of system level design. Proc. IEEE 95(3), 467–506 (2007)

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  49. Tripakis, S., Lickly, B., Henzinger, T.A., Lee, E.A.: A theory of synchronous relational interfaces. Trans. Program. Lang. Syst. 33(4), 14 (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Electrical Engineering, University of Southern California, Los Angeles, CA, 90089, USA

    Pierluigi Nuzzo

  2. Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, Berkeley, CA, 94720, USA

    Alberto L. Sangiovanni-Vincentelli

Authors
  1. Pierluigi Nuzzo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alberto L. Sangiovanni-Vincentelli
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pierluigi Nuzzo .

Editor information

Editors and Affiliations

  1. University of California, Berkeley, Berkeley, California, USA

    Marten Lohstroh

  2. National Instruments, Berkeley, California, USA

    Patricia Derler

  3. Mälardalen University, Västerås, Sweden, Reykjavík University, Reykjavik, Iceland

    Marjan Sirjani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Nuzzo, P., Sangiovanni-Vincentelli, A.L. (2018). Hierarchical System Design with Vertical Contracts. In: Lohstroh, M., Derler, P., Sirjani, M. (eds) Principles of Modeling. Lecture Notes in Computer Science(), vol 10760. Springer, Cham. https://doi.org/10.1007/978-3-319-95246-8_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95246-8_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95245-1

  • Online ISBN: 978-3-319-95246-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation