Structural Contracts – Motivating Contracts to Ensure Extra-Functional Semantics

  • Gregor Nitsche
  • Ralph Görgen
  • Kim Grüttner
  • Wolfgang Nebel
Conference paper
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT, volume 523)

Abstract

In our work we aim at a composable and consistent specification and verification of contracts for extra-functional properties, such as power consumption or temperature. To this end, a necessary precondition for the semantical correctness of such properties is to ensure the structurally correct modeling of their interdependences.

While this can be solved by a tailoring of the Component Based Design (CmpBD) frameworks, the resulting design constraints are specific to tools and viewpoints, not being sufficiently configurable for the designers. To solve this problem within the contract framework, Contract Based Design (CBD) with explicit port variables provides also no configurable but sound methodology for structurally relating the properties between different components and views. For that, we propose the idea of structural contracts. Using implicit structural ports, structural guarantees can be given according to the Component Based Design structure. Expressing structural design constraints by the means of structural assumptions, the CmpBD constraints can become part of the Contract Based Design framework and, thus, can be checked for compatibility and refinement.

As a result, structural contracts enable the contract based specification and verification of structural rules for the correct modeling of functional and extra-functional interdependences. Providing both, property specifications and Component Based Design constraints by contracts, the approach is flexible and sound.

Keywords

Contracts Contract based design Components Component based design Compositionality Composability Compatibility Structure Extra-functional View Aspect Type Semantics 

References

  1. 1.
    de Alfaro, L., Henzinger, T.: Interface-based design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, T. (eds.) Engineering Theories of Software Intensive Systems, NATO Science Series, vol. 195. Springer, Netherlands (2005).  https://doi.org/10.1007/1-4020-3532-2_3CrossRefGoogle Scholar
  2. 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_11CrossRefGoogle Scholar
  3. 3.
    Benveniste, A., Caillaud, B., Nickovic, D., Passerone, R., Raclet, J.B., Reinkemeier, P., Sangiovanni-Vincentelli, A., Damm, W., Henzinger, T., Larsen, K.: Contracts for systems design. Technical Report RR-8147, Research Centre Rennes - Bretagne Atlantique, Rennes Cedex (2012)Google Scholar
  4. 4.
    Bliudze, S., Sifakis, J.: A notion of glue expressiveness for component-based systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 508–522. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85361-9_39CrossRefGoogle Scholar
  5. 5.
    Bliudze, S., Sifakis, J.: Synthesizing glue operators from glue constraints for the construction of component-based systems. In: Apel, S., Jackson, E. (eds.) SC 2011. LNCS, vol. 6708, pp. 51–67. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22045-6_4CrossRefGoogle Scholar
  6. 6.
    Cardelli, L.: Type systems. ACM Comput. Surv. 28(1), 263–264 (1996)CrossRefGoogle Scholar
  7. 7.
    Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: 28th IEEE/ACM International Conference on Automated Software Engineering (ASE) (2013)Google Scholar
  8. 8.
    Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Validation of requirements for hybrid systems: a formal approach. ACM Trans. Softw. Eng. Methodol. (TOSEM) 21(4), 22 (2012)CrossRefGoogle Scholar
  9. 9.
    Lee, E.A., Sangiovanni-Vincentelli, A.L.: Component-based design for the future. In: Design, Automation & Test in Europe (DATE) (2011)Google Scholar
  10. 10.
    Nitsche, G.: Structural contracts - conceptual example in OCRA. https://vhome.offis.de/gnitsche/paper/iess2015/example/
  11. 11.
    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)MathSciNetCrossRefGoogle Scholar
  12. 12.
    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)MATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2017

Authors and Affiliations

  1. 1.OFFIS – Institute for Information TechnologyOldenburgGermany
  2. 2.Carl von Ossietzky University OldenburgOldenburgGermany

Personalised recommendations