Abstract
The purpose of this paper is to present a framework to model component interfaces and the component connectors that provide the glue code for the components. Our modeling approach is based on two input languages which rely on the same automata model. One of them is a scripting language which can serve to specify exogenous or endogenous coordination mechanisms. The other one is a guarded command language which has been designed to specify behavioral component interfaces, but can also be used to design component connectors. This hybrid approach allows nesting of the two specification languages, supports compositional design, modular verification and reusability of components or component connectors. It yields the input language of our verification toolset Vereofy which realizes several model checking algorithms for components, component connectors, and the composite system.
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
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T.: Reactive Modules. Formal Methods in System Design: An Intern. J. 15(1), 7–48 (1999)
Arbab, F.: Reo: A Channel-Based Coordination Model for Component Composition. MSCS 14(3), 329–366 (2004)
Arbab, F., Sun, M., Baier, C.: Synthesis of Reo circuits from scenario-based specifications. In: FOCLASA 2008. ENTCS (2008) (to appear)
Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: Formal verification for components and connectors (submitted for publication)
Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling Component Connectors in Reo by Constraint Automata. SCP 61, 75–113 (2006)
Blechmann, T., Baier, C.: Checking equivalence for reo networks. In: FACS 2007. ENTCS, vol. 215, pp. 209–226 (2008)
Blechmann, T., Klein, J., Klüppelholz, S.: Vereofy, http://www.vereofy.de/
Capizzi, S., Solmi, R., Zavattaro, G.: From endogenous to exogenous coordination using aspect-oriented programming. In: De Nicola, R., Ferrari, G.-L., Meredith, G. (eds.) COORDINATION 2004. LNCS, vol. 2949. Springer, Heidelberg (2004)
de Alfaro, L., Dias da Silva, L., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable interfaces. In: Gramlich, B. (ed.) FroCos 2005. LNCS, vol. 3717, pp. 81–105. Springer, Heidelberg (2005)
de Alfaro, L., Henzinger, T.: 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)
Gelernter, D., Carriero, N., Chandran, S., Chang, S.: Parallel programming in linda. In: ICPP, pp. 255–263 (1985)
Gößler, G., Sifakis, J.: Component-based construction of deadlock-free systems: Extended abstract. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 420–433. Springer, Heidelberg (2003)
Guillen-Scholten, J., Arbab, F., de Boer, F., Bonsangue, M.: MoCha-pi: an exogenous coordination calculus based on mobile channels. In: Proceedings of the 2005 ACM symposium on Applied computing (SAC), pp. 436–442. ACM, New York (2005)
Klüppelholz, S., Baier, C.: Symbolic Model Checking for Channel-based Component Connectors. In: Science of Computer Programming (2009)
Klüppelholz, S., Baier, C.: Alternating-time stream logic for multi-agent systems. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 184–198. Springer, Heidelberg (2008)
Lynch, N., Tuttle, M.: An Introduction to Input/Output Automata. CWI Quarterly 2(3), 219–246 (1989)
Majster-Cederbaum, M., Minnameier, C.: Everything is PSPACE-complete in interaction systems. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 216–227. Springer, Heidelberg (2008)
Milner, R.: Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, Cambridge (1999)
Reo website at CWI Amsterdam, http://reo.project.cwi.nl/
Scholten, J.-G., Arbab, F., de Boer, F., Bonsangue, M.: Modeling the exogenous coordination of mobile channel-based systems with Petri nets. In: FOCLASA 2005. ENTCS, vol. 154(1), pp. 83–99 (2006)
Sirjani, M., Jaghoori, M., Baier, C., Arbab, F.: Compositional semantics of an actor-based language using constraint automata. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 281–297. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 IFIP International Federation for Information Processing
About this paper
Cite this paper
Baier, C., Blechmann, T., Klein, J., Klüppelholz, S. (2009). A Uniform Framework for Modeling and Verifying Components and Connectors. In: Field, J., Vasconcelos, V.T. (eds) Coordination Models and Languages. COORDINATION 2009. Lecture Notes in Computer Science, vol 5521. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02053-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-02053-7_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02052-0
Online ISBN: 978-3-642-02053-7
eBook Packages: Computer ScienceComputer Science (R0)