Skip to main content
SpringerLink
Log in
Book cover

Formal Aspects of Component Software

FACS 2015: Formal Aspects of Component Software pp 294–311Cite as

Typed Connector Families

  • Conference paper
  • First Online:

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

Abstract

Typed models of connector/component composition specify interfaces describing ports of components and connectors. Typing ensures that these ports are plugged together appropriately, so that data can flow out of each output port and into an input port. These interfaces typically consider the direction of data flow and the type of values flowing. Components, connectors, and systems are often parameterised in such a way that the parameters affect the interfaces. Typing such connector families is challenging. This paper takes a first step towards addressing this problem by presenting a calculus of connector families with integer and boolean parameters. The calculus is based on monoidal categories, with a dependent type system that describes the parameterised interfaces of these connectors. As an example, we demonstrate how to define n-ary Reo connectors in the calculus. The paper focusses on the structure of connectors—well-connectedness—and less on their behaviour, making it easily applicable to a wide range of coordination and component-based models. A type-checking algorithm based on constraints is used to analyse connector families, supported by a proof-of-concept implementation.

This research is supported by the FCT grant SFRH/BPD/91908/2012.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    Known as \(\beta \)-reduction in lambda calculus.

  2. 2.

    https://github.com/joseproenca/parameterised-connectors.

  3. 3.

    http://choco-solver.org.

References

  1. Apel, S., Speidel, H., Wendler, P., von Rhein, A., Beyer, D.: Detection of feature interactions using feature-aware verification. In: Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, pp. 372–375. IEEE Computer Society, Washington, DC (2011)

    Google Scholar 

  2. Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  3. Arbab, F., Bruni, R., Clarke, I., Lanese, I., Montanari, U.: Tiles for Reo. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 37–55. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Bonchi, F., Sobocinski, P., Zanasi, F.: Full abstraction for signal flow graphs. In: Proceedings of the 42nd Annual Symposium on Principles of Programming Languages, POPL 2015, pp. 515–526. ACM, New York (2015)

    Google Scholar 

  5. Bruni, R., Lanese, I., Montanari, U.: A basic algebra of stateless connectors. Theor. Comput. Sci. 366(1–2), 98–120 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  6. Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions: Trading precision for speed in family-based analyses (extended version) CoRR. abs/1503.04608 (2015)

    Google Scholar 

  7. Gadducci, F., Montanari, U.: The tile model. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 133–166. The MIT Press (2000)

    Google Scholar 

  8. Gibbons, J.: A pointless derivation of radix sort. J. Funct. Program. 9(3), 339–346 (1999)

    Article  MATH  Google Scholar 

  9. Jones, M.P.: A theory of qualified types. Sci. Comput. Program. 22(3), 231–256 (1994)

    Article  MATH  Google Scholar 

  10. Kastner, C., Apel, S.: Type-checking software product lines - a formal approach. In: Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2008, pp. 258–267. IEEE Computer Society, Washington, DC (2008)

    Google Scholar 

  11. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  12. Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering. Springer, Heidelberg (2005)

    Book  MATH  Google Scholar 

  13. Post, H., Sinz, C., Configuration lifting,: Verification meets software configuration. In Proceedings of the 23rd International Conference on Automated Software Engineering, ASE ’08, pp. 347–350. IEEE Computer Society, 2008. (2008)

    Google Scholar 

  14. Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics. Lecture Notes in Physics, vol. 813, pp. 289–355. Springer, Berlin Heidelberg (2011)

    Chapter  Google Scholar 

  15. Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics. Lecture Notes in Physics, vol. 813, pp. 289–355. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Thaker, S., Batory, D., Kitchin, D., Cook, W.: Safe composition of product lines. In Proceedings of the 6th International Conference on Generative Programming and Component Engineering, GPCE 2007, pp. 95–104. ACM (2007)

    Google Scholar 

  17. Thüm, T., Schaefer, I., Apel, S., Hentschel, M.: Family-based deductive verification of software product lines. In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering, GPCE 2012, pp. 11–20. ACM, New York (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. HASLab – INESC TEC and Universidade Do Minho, Braga, Portugal

    José Proença

  2. IMinds-DistriNet, Department of Computer Science, Ku Leuven, Belgium

    José Proença

  3. Department of Information Technology, Uppsala University, Uppsala, Sweden

    Dave Clarke

Authors
  1. José Proença
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dave Clarke
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to José Proença .

Editor information

Editors and Affiliations

  1. Universidade Federal Fluminense, Niterói, Brazil

    Christiano Braga

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Proença, J., Clarke, D. (2016). Typed Connector Families. In: Braga, C., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2015. Lecture Notes in Computer Science(), vol 9539. Springer, Cham. https://doi.org/10.1007/978-3-319-28934-2_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-28934-2_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-28933-5

  • Online ISBN: 978-3-319-28934-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation