Skip to main content
SpringerLink
Log in

Modeling and Analysis of Component Connectors in Coq

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2013)

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

Included in the following conference series:

Abstract

Connectors have emerged as a powerful concept for composition and coordination of concurrent activities encapsulated as components and services. Compositional coordination languages, like Reo, serve as a means to formally specify and implement connectors. They support large-scale distributed applications by allowing construction of complex component connectors out of simpler ones. In this paper, we present a new approach to modeling and analysis of Reo connectors via Coq, a proof assistant based on high-order logic and \(\lambda \)-calculus. Basic notions in Reo, like nodes and channels, are defined by inductive types. By tracing the data streams, we can simulate the behavior and output of a given Reo connector. Besides, with prerequisite axioms given, we can automatically prove connectors’ properties using the Coq proof assistant.

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.

    This connector is a simplification of one example provided in [17].

References

  1. Aichernig, B.K., Arbab, F., Astefanoaei, L., de Boer, F.S., Meng, S., Rutten, J.J.M.M.: Fault-based test case generation for component connectors. In: Proceedings of TASE 2009, pp. 147–154. IEEE Computer Society (2009)

    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., Baier, C., de Boer, F., Rutten, J.: Models and temporal logical specifications for timed component connectors. Softw. Syst. Model. 6(1), 59–82 (2007)

    Article  Google Scholar 

  4. Arbab, F., Chothia, T., Meng, S., Moon, Y.-J.: Component connectors with QoS guarantees. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 286–304. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Arbab, F., Chothia, T., van der Mei, R., Meng, S., Moon, Y.J., Verhoef, C.: From coordination to stochastic models of QoS. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 268–287. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Arbab, F., Koehler, C., Maraikar, Z., Moon, Y.-J., Proença, J.: Modeling, testing and executing Reo connectors with the eclipse coordination tools. In: Preliminary proceedings of FACS 2008 (2008)

    Google Scholar 

  7. Arbab, F., Meng, S., Moon, Y.-J., Kwiatkowska, M., Qu, H.: Reo2mc: a tool chain for performance analysis of coordination models. In: Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, pp. 287–288. ACM (2009)

    Google Scholar 

  8. Arbab, F., Rutten, J.J.M.M.: A coinductive calculus of component connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 34–55. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S., Leister, W.: Design and verification of systems with exogenous coordination using vereofy. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 97–111. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61, 75–113 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  11. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2004)

    Book  Google Scholar 

  12. Ciancarini, P.: Coordination models and languages as software integrators. ACM Comput. Surv. (CSUR) 28(2), 300–302 (1996)

    Article  Google Scholar 

  13. Clarke, D., Costa, D., Arbab, F.: Connector colouring I: synchronisation and context dependency. Sci. Comput. Program. 66, 205–225 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  14. Eclipse Coordination Tools. http://reo.project.cwi.nl/

  15. Halpern, J.Y., Vardi, M.Y.: Model checking vs. theorem proving: a manifesto. In: Artificial intelligence and mathematical theory of computation, pp. 151–176. Academic Press Professional, San Diego (1991)

    Google Scholar 

  16. Khosravi, R., Sirjani, M., Asoudeh, N., Sahebi, S., Iravanchi, H.: Modeling and analysis of Reo connectors using alloy. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 169–183. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Kokash, N., Arbab, F.: Formal design and verification of long-running transactions with eclipse coordination tools. IEEE Trans. Serv. Comput. 6(2), 186–200 (2013)

    Article  Google Scholar 

  18. Kokash, N., Krause, Ch., de Vink, E.: Reo \(+\) mCRL2: a framework for model-checking dataflow in service compositions. Formal Aspects Comput. 24(2), 187–216 (2012)

    Article  MATH  Google Scholar 

  19. Meng, S.: Connectors as designs: the time dimension. In: Proceedings of TASE 2012, pp. 201–208. IEEE Computer Society (2012)

    Google Scholar 

  20. Meng, S., Arbab, F., Aichernig, B.K., Aştefănoaei, L., de Boer, F.S., Rutten, J.: Connectors as designs: modeling, refinement and test case generation. Sci. Comput. Program. 77(7), 799–822 (2012)

    Article  MATH  Google Scholar 

  21. Mousavi, M.R., Sirjani, M., Arbab, F.: Formal semantics and analysis of component connectors in Reo. Electron. Notes Theor. Comput. Sci. 154(1), 83–99 (2006)

    Article  Google Scholar 

  22. Ramasubbu, N., Balan, R.K.: Globally distributed software development project performance: an empirical analysis. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, pp. 125–134. ACM (2007)

    Google Scholar 

  23. Source code of the Coq development. http://www.math.pku.edu.cn/teachers/sunm/rc/Main.v

Download references

Acknowledgement

The work was partially supported by the National Natural Science Foundation of China under grant no. 61202069 and 61272160, and Research Fund for the Doctoral Program of Higher Education of China under grant no. 201200011 20103.

Author information

Authors and Affiliations

  1. LMAM and Department of Informatics, School of Mathematical Sciences, Peking University, Beijing, China

    Yi Li & Meng Sun

Authors
  1. Yi Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Meng Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Meng Sun .

Editor information

Editors and Affiliations

  1. Royal Holloway University of London, Egham, United Kingdom

    José Luiz Fiadeiro

  2. Birmingham City University, Birmingham, United Kingdom

    Zhiming Liu

  3. Jiangxi Normal University, Lab. High-Performance Computing, Nanchang, China

    Jinyun Xue

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Li, Y., Sun, M. (2014). Modeling and Analysis of Component Connectors in Coq. In: Fiadeiro, J., Liu, Z., Xue, J. (eds) Formal Aspects of Component Software. FACS 2013. Lecture Notes in Computer Science(), vol 8348. Springer, Cham. https://doi.org/10.1007/978-3-319-07602-7_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-07602-7_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-07601-0

  • Online ISBN: 978-3-319-07602-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation