{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T05:12:57Z","timestamp":1771045977281,"version":"3.50.1"},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2008,11,30]],"date-time":"2008-11-30T00:00:00Z","timestamp":1228003200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGMETRICS Perform. Eval. Rev."],"published-print":{"date-parts":[[2008,11,30]]},"abstract":"<jats:p>In this paper we explore the practical possibilities of using formal methods to analyze gossiping networks. In particular, we use \u03bcCRL and Groove to model the peer sampling service, and analyze it through a series of model transformations to CTMCs and finally MRMs. Our tools compute the expected value of various network quality indicators, such as average path lengths, over all possible system runs. Both transient and steady state analysis are supported. We compare our results with the simulation and emulation results found in [10].<\/jats:p>","DOI":"10.1145\/1481506.1481510","type":"journal-article","created":{"date-parts":[[2008,12,30]],"date-time":"2008-12-30T17:45:31Z","timestamp":1230659131000},"page":"7-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Applying formal methods to gossiping networks with mCRL and groove"],"prefix":"10.1145","volume":"36","author":[{"given":"Pepijn","family":"Crouzen","sequence":"first","affiliation":[{"name":"Saarland University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[{"name":"University of Twente"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arend","family":"Rensink","sequence":"additional","affiliation":[{"name":"University of Twente"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,11,30]]},"reference":[{"key":"e_1_2_1_1_1","series-title":"LNCS","first-page":"780","volume-title":"ICALP","author":"Baier C.","year":"2000"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1317379.1317385"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"key":"e_1_2_1_4_1","series-title":"LNCS","first-page":"250","volume-title":"CAV","author":"Blom S.","year":"2001"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/43921.43922"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2004.1297243"},{"key":"e_1_2_1_7_1","series-title":"LNCS","first-page":"410","volume-title":"L.-H","author":"Garavel H.","year":"2002"},{"key":"e_1_2_1_8_1","series-title":"LNCS","first-page":"38","volume-title":"Euro Summer School on Trends in Computer Science","author":"Haverkort B.","year":"2000"},{"key":"e_1_2_1_9_1","volume-title":"PAPM","author":"Hermanns H.","year":"1996"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275517.1275520"},{"key":"e_1_2_1_11_1","series-title":"LNCS (Tutorial Volume)","first-page":"220","volume-title":"SFM-07:PE","author":"Kwiatkowska M.","year":"2007"},{"key":"e_1_2_1_12_1","series-title":"BRICS Notes Series","volume-title":"STTT","author":"Mateescu R.","year":"1998"},{"key":"e_1_2_1_13_1","unstructured":"R. Milner Communicating and Mobile Systems; The Pi Calculus. Cambridge University Press 1999.   R. Milner Communicating and Mobile Systems; The Pi Calculus . Cambridge University Press 1999."},{"key":"e_1_2_1_14_1","series-title":"LNCS","first-page":"376","volume-title":"CAV","author":"Nicollin X.","year":"1991"},{"key":"e_1_2_1_15_1","series-title":"LNCS","first-page":"479","volume-title":"AGTIVE","author":"Rensink A.","year":"2004"},{"key":"e_1_2_1_16_1","series-title":"Electronic Communications of the EASST","volume-title":"A","author":"Rensink A.","year":"2007"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/774763.774784"}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481506.1481510","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1481506.1481510","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:09Z","timestamp":1750253409000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481506.1481510"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11,30]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,11,30]]}},"alternative-id":["10.1145\/1481506.1481510"],"URL":"https:\/\/doi.org\/10.1145\/1481506.1481510","relation":{},"ISSN":["0163-5999"],"issn-type":[{"value":"0163-5999","type":"print"}],"subject":[],"published":{"date-parts":[[2008,11,30]]},"assertion":[{"value":"2008-11-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}