Abstract
This paper is an extended version of the Credo Methodology [16]. Credo offers tools and techniques to model and analyze highly reconfigurable distributed systems. In a previous version we presented an integrated methodology to use the Credo tool suite. Following a compositional, component–based approach to model and analyze distributed systems, we presented a separation of the system into components and the network. A high–level, abstract representation of the dataflow level on the network was given in terms of behavioral interface automata and a detailed model of the components in terms of Creol models. Here we extend the methodology with a detailed model of the network connecting these components. The Vereofy tool set is used to model and analyze the dataflow of the network in detail. The behavioral automata connect the detailed model of the network and the detailed model of the components. We apply the extended methodology to our running example, a peer-to-peer file-sharing system.
This work has been funded by the European IST-33826 STREP project CREDO on Modeling and Analysis of Evolutionary Structures for Distributed Services. ( http://credo.cwi.nl )
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aichernig, B., Griesmayer, A., Schlatte, R., Stam, A.: Modeling and testing multi-threaded asynchronous systems with Creol. In: Proc. TTSS 2008. ENTCS, vol. 243, pp. 3–14. Elsevier, Amsterdam (2009)
The Almende research company, http://www.almende.com/
Arbab, F.: Reo: A channel-based coordination model for component composition. Mathematical Structures in Computer Science 14, 329–366 (2004)
Arbab, F., Baier, C., Rutten, J.J., Sirjani, M.: Modeling component connectors in Reo by constraint automata. In: Proc. FOCLASA 2003. ENTCS, vol. 97, pp. 25–46. Elsevier, Amsterdam (2004)
Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: Formal Verification for Components and Connectors. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 82–101. Springer, Heidelberg (2009)
Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: A Uniform Framework for Modeling and Verifying Components and Connectors. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 247–267. Springer, Heidelberg (2009)
Baier, C., Sirjani, M., Arbab, F., Rutten, J.J.M.M.: Modeling Component Connectors in Reo by Constraint Automata. In: Proceedings of the 2nd International Workshop on Foundations of Coordination Languages and Software Architectures. Science of Computer Programming, vol. 61, pp. 75–113 (2006)
Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST, pp. 125–126. IEEE Computer Society, Los Alamitos (2006)
Blechmann, T., Baier, C.: Checking equivalence for Reo networks. In: Electronic Notes in Theoretical Computer Science, vol. 215, pp. 209–226 (2008)
Blechmann, T., Klein, J., Klüppelholz, S.: Vereofy, http://www.vereofy.de
Blechmann, T., Klein, J., Klüppelholz, S.: Vereofy User Manual. TU Dresden (2008 –2009), http://www.vereofy.de
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science (2001)
CWI Coordination Group. Eclipse coordination tools, http://reo.project.cwi.nl/cgi-bin/trac.cgi/reo/wiki/Tools
de Boer, F., Chothia, T., Jaghoori, M.M.: Modular schedulability analysis of concurrent objects in Creol. In: Arbab, F., Sirjani, M. (eds.) Fundamentals of Software Engineering. LNCS, vol. 5961, pp. 212–227. Springer, Heidelberg (2010)
de Boer, F.S., Grabe, I., Jaghoori, M.M., Stam, A., Yi, W.: Modeling and Analysis of Thread-Pools in an Industrial Communication Platform. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 367–386. Springer, Heidelberg (2009)
Grabe, I., Jaghoori, M.M., Aichernig, B., Baier, C., Blechmann, T., de Boer, F., Griesmayer, A., Johnsen, E.B., Klein, J., Klüppelholz, S., Kyas, M., Leister, W., Schlatte, R., Stam, A., Steffen, M., Tschirner, S., Liang, X., Yi, W.: Credo methodology. Modeling and analyzing a peer-to-peer system in Credo. In: Johnsen, E.B., Stolz, V. (eds.) Proceedings of the 3nd International Workshop on Harnessing Theories for Tool Support in Software (TTSS 2009), ICTAC 2009 satellite Workshop. Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2010)
Grabe, I., Steffen, M., Torjusen, A.B.: Executable Interface Specifications for Testing Asynchronous Creol Components. In: Arbab, F., Sirjani, M. (eds.) Fundamentals of Software Engineering. LNCS, vol. 5961, pp. 324–339. Springer, Heidelberg (2010)
Griesmayer, A., Aichernig, B.K., Johnsen, E.B., Schlatte, R.: Dynamic symbolic execution for testing distributed objects. In: Dubois, C. (ed.) Tests and Proofs. LNCS, vol. 5668, pp. 105–120. Springer, Heidelberg (2009)
Jaghoori, M.M.: Coordinating object oriented components using data-flow networks. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 280–311. Springer, Heidelberg (2008)
Jaghoori, M.M., de Boer, F.S., Chothia, T., Sirjani, M.: Schedulability of asynchronous real-time concurrent objects. J. Logic and Alg. Prog. 78(5), 402–416 (2009)
Jaghoori, M.M., Longuet, D., de Boer, F.S., Chothia, T.: Schedulability and compatibility of real time asynchronous objects. In: Proc. Real Time Systems Symposium, pp. 70–79. IEEE Computer Society Press, Los Alamitos (2008)
Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling 6(1), 35–58 (2007)
Klüppelholz, S., Baier, C.: Alternating-time stream logic for multi-agent systems. Science of Computer Programming. Corrected Proof (2009) (in Press)
Klüppelholz, S., Baier, C.: Symbolic model checking for channel-based component connectors. Science of Computer Programming 74(9), 688–701 (2009)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1-2), 134–152 (1997)
Leister, W., Björk, J., Schlatte, R., Griesmayer, A.: Validation of Creol models for routing algorithms in wireless sensor networks. Report 1024, Norsk Regnesentral, Oslo, Norway (2010)
Leister, W., Liang, X., Klüppelholz, S., Klein, J., Owe, O., Kazemeyni, F., Bjørk, J., Østvold, B.M.: Modelling of biomedical sensor networks using the Creol tools. Report 1022, Norsk Regnesentral, Oslo, Norway (2009)
Rumpe, B., Klein, C.: Automata describing object behavior. In: Object-Oriented Behavioral Specifications, pp. 265–286. Springer, Heidelberg (1996)
Tschirner, S., Xuedong, L., Yi, W.: Model-based validation of QoS properties of biomedical sensor networks. In: Proc. Embedded software (EMSOFT 2008), pp. 69–78. ACM Press, New York (2008)
Vereofy source code of the peer-to-peer example (2010), http://www.vereofy.de/download/examples/vereofy_p2p_example.zip
Yu, I.C., Johnsen, E.B., Owe, O.: Type-safe runtime class upgrades in Creol. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 202–217. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grabe, I. et al. (2010). The Credo Methodology. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds) Formal Methods for Components and Objects. FMCO 2009. Lecture Notes in Computer Science, vol 6286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17071-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-17071-3_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17070-6
Online ISBN: 978-3-642-17071-3
eBook Packages: Computer ScienceComputer Science (R0)