Abstract
Reo is a channel-based exogenous coordination model in which complex coordinators, called connectors, are compositionally built out of simpler ones. In this paper, we present a new approach to model connectors in Coq which is a proof assistant based on higher-order logic and \(\lambda \)-calculus. The model reflects the original structure of connectors simply and clearly. In our framework, basic connectors (channels) are interpreted as axioms and composition operations are specified as inference rules. Furthermore, connectors are interpreted as logical predicates which describe the relation between inputs and outputs. With such definitions provided, connector properties, as well as equivalence and refinement relations between different connectors, can be naturally formalized as goals in Coq and easily proved using pre-defined tactics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
If we use \(\alpha ,\beta \) to denote the data streams that flow through the channel ends of a channel and a, b to denote the time stream corresponding to the data streams, i.e., the i-th element a(i) in a denotes exactly the time moment of the occurrence of \(\alpha (i)\), then we can easily obtain the specifications for different channels, as discussed in [17, 19]. For example, a synchronous channel can be expressed as \(\alpha =\beta \wedge a =b \).
References
Package of source files. https://github.com/liyi-david/reoincoq
Aichernig, B.K., Arbab, F., Astefanoaei, L., de Boer, F.S., Sun, M., Rutten, J.: Fault-based test case generation for component connectors. In: Proceedings of TASE 2009, pp. 147–154. IEEE Computer Society (2009)
Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004)
Arbab, F., Rutten, J.J.M.M.: A coinductive calculus of component connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2002. LNCS, vol. 2755, pp. 34–55. Springer, Heidelberg (2003). doi:10.1007/978-3-540-40020-2_2
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. LNCS, vol. 6416, pp. 97–111. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16561-0_15
Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61, 75–113 (2006)
Clarke, D., Costa, D., Arbab, F.: Modelling coordination in biological systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 9–25. Springer, Heidelberg (2006). doi:10.1007/11925040_2
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, New York (1998)
Huet, G., Kahn, G., Paulin-Mohring, C.: The coq proof assistant a tutorial. Rapport Technique, 178 (1997)
Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall, Upper Saddle River (1990)
Jongmans, S.T.Q., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comp. Sci. 22(1), 201–251 (2012)
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). doi:10.1007/978-3-540-68265-3_11
Klüppelholz, S., Baier, C.: Symbolic model checking for channel-based component connectors. Sci. Comput. Program. 74(9), 688–701 (2009)
Kokash, N., Krause, C., de Vink, E.: Reo+mCRL2: a framework for model-checking dataflow in service compositions. Formal Aspects Comput. 24, 187–216 (2012)
Li, Y., Sun, M.: Modeling and verification of component connectors in Coq. Sci. Comput. Program. 113(3), 285–301 (2015)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1998)
Sun, M.: Connectors as designs: the time dimension. In: Proceedings of TASE 2012, pp. 201–208. IEEE Computer Society (2012)
Sun, M., Arbab, F.: Web services choreography and orchestration in reo and constraint automata. In: Proceedings of SAC 2007, pp. 346–353. ACM (2007)
Sun, M., Arbab, F., Aichernig, B.K., Astefanoaei, L., de Boer, F.S., Rutten, J.: Connectors as designs: modeling, refinement and test case generation. Sci. Comput. Program. 77(7–8), 799–822 (2012)
Acknowledgement
The work was partially supported by the National Natural Science Foundation of China under grant no. 61532019, 61202069 and 61272160.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Zhang, X., Hong, W., Li, Y., Sun, M. (2017). Reasoning About Connectors in Coq. In: Kouchnarenko, O., Khosravi, R. (eds) Formal Aspects of Component Software. FACS 2016. Lecture Notes in Computer Science(), vol 10231. Springer, Cham. https://doi.org/10.1007/978-3-319-57666-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-57666-4_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57665-7
Online ISBN: 978-3-319-57666-4
eBook Packages: Computer ScienceComputer Science (R0)