Abstract
In distributed and mobile systems with volatile bandwidth and fragile connectivity, non-functional aspects like performance and reliability become more and more important. To formalise, measure, and predict these properties, stochastic methods are required. At the same time such systems are characterised by a high degree of architectural reconfiguration. Viewing the architecture of a distributed system as a graph, this is naturally modelled by graph transformations.
To address these two concerns, stochastic graph transformation systems have been introduced associating with each rule its application rate—the rate of the exponential distribution governing the delay of its application. Deriving continuous-time Markov chains, Continuous Stochastic Logic is used to specify reliability properties and verify them through model checking.
In particular, we study a protocol for the reconfiguration of P2P networks intended to improve their reliability by adding redundant connections. The modelling of this protocol as a (stochastic) graph transformation system takes advantage of negative application and conditions path expressions. This ensuing high-level style of specification helps to reduce the number of states and increases the capabilities for automated analysis.
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
Ajmone-Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley Series in Parallel Computing. John Wiley and Sons, Chichester (1995)
Anderson, W.G.: Continuous-Time Markov Chains. Springer, Heidelberg (1991)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model checking continuous-time markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)
Bause, F., Kritzinger, P.S.: Stochastic Petri Nets, 2nd edn. Vieweg Verlag (2002)
Brinksma, E., Hermanns, H.: Process algebra and Markov chains. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 183–231. Springer, Heidelberg (2001)
Corradini, A., Montanari, U., Rossi, F.: Graph processes. Fundamenta Informaticae 26(3,4), 241–266 (1996)
D’Argenio, P.R.: Algebras and Automata for Timed and Stochastic Systems. IPA Dissertation Series 1999-10, CTIT PhD-Thesis Series 99-25, University of Twente (November 1999)
Ehrig, H., Pfender, M., Schneider, H.J.: Graph grammars: an algebraic approach. In: 14th Annual IEEE Symposium on Switching and Automata Theory, pp. 167–180. IEEE, Los Alamitos (1973)
Gilb, T.: Principles of Software Engineering Management. Addison-Wesley, Reading (1988)
Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundamenta Informaticae 26(3,4), 287–313 (1996)
Heckel, R., Lajios, G., Menge, S.: Stochastic graph transformation systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 210–225. Springer, Heidelberg (2004)
Heckel, R., Lajios, G., Menge, S.: Modulare Analyse Stochastischer Graphtransformationssysteme. In: Liggesmeyer, P., Pohl, K., Goedicke, M. (eds.) Software Engineering 2005, Essen, Germany, GI, March 2005. Lecture Notes in Informatics, vol. 64, pp. 141–152 (2005)
Korff, M., Ribeiro, L.: Concurrent derivations as single pushout graph grammar processes. In: Proc. Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation (SEGRAGRA). Electronic Notes in TCS, vol. 2, pp. 113–122. Elsevier Science, Amsterdam (1995)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)
Löwe, M.: Algebraic approach to single-pushout graph transformation. Theoret. Comput. Sci. 109, 181–224 (1993)
Mariani, L.: Fault-tolerant routing for p2p systems with unstructured topology. In: Proc. International Symposium on Applications and the Internet (SAINT 2005), Trento (Italy). IEEE Computer Society, Los Alamitos (2005)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96, 73–155 (1992)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Molloy, M.K.: On the Integration of Delay and Throughput Measures in Distributed Processing Models. PhD thesis, University of California (1981)
Natkin, S.: Les Réseaux de Petri Stochastiques et leur Application à l’Evaluation des Systémes Informatiques. PhD thesis, CNAM Paris (1980)
Norris, J.R.: Markov Chains. Cambridge University Press, Cambridge (1997)
Priami, C.: Stochastic π-calculus. The Computer Journal 38, 578–589 (1995); Proc. PAPM 1995
Rensink, A.: The GROOVE simulator: A tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004)
Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation, Foundations, vol. 1. World Scientific, Singapore (1997)
Stewart, W.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)
University of Paderborn Software Engineering Group. The Fujaba Tool Suite, http://www.fujaba.de
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heckel, R. (2005). Stochastic Analysis of Graph Transformation Systems: A Case Study in P2P Networks. In: Van Hung, D., Wirsing, M. (eds) Theoretical Aspects of Computing – ICTAC 2005. ICTAC 2005. Lecture Notes in Computer Science, vol 3722. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560647_4
Download citation
DOI: https://doi.org/10.1007/11560647_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29107-7
Online ISBN: 978-3-540-32072-2
eBook Packages: Computer ScienceComputer Science (R0)