{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T17:56:28Z","timestamp":1725818188300},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319155449"},{"type":"electronic","value":"9783319155456"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15545-6_16","type":"book-chapter","created":{"date-parts":[[2015,3,5]],"date-time":"2015-03-05T02:19:15Z","timestamp":1425521955000},"page":"231-252","source":"Crossref","is-referenced-by-count":2,"title":["Formal Analysis of Leader Election in MANETs Using Real-Time Maude"],"prefix":"10.1007","author":[{"given":"Si","family":"Liu","sequence":"first","affiliation":[]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"16_CR1","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"G. Agha","year":"2006","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. Electronic Notes in Theoretical Computer Science\u00a0153(2), 213\u2013239 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"16_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A. Bouhoula","year":"2000","unstructured":"Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theoretical Computer Science\u00a0236(1-2), 35\u2013132 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"16_CR4","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1002\/wcm.72","volume":"2","author":"T. Camp","year":"2002","unstructured":"Camp, T., Boleng, J., Davies, V.: A survey of mobility models for ad hoc network research. Wireless Communications and Mobile Computing\u00a02(5), 483\u2013502 (2002)","journal-title":"Wireless Communications and Mobile Computing"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"16_CR6","unstructured":"Fall, K., Varadhan, K.: The ns Manual (2011), \n \n http:\/\/www.isi.edu\/nsnam\/ns\/doc\/ns_doc.pdf"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Gelastou, M., Georgiou, C., Philippou, A.: On the application of formal methods for specifying and verifying distributed protocols. In: Proc. NCA 2008. IEEE (2008)","DOI":"10.1109\/NCA.2008.24"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-40213-5_14","volume-title":"Fundamentals of Software Engineering","author":"F. Ghassemi","year":"2013","unstructured":"Ghassemi, F., Ahmadi, S., Fokkink, W., Movaghar, A.: Model checking MANETs with arbitrary mobility. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol.\u00a08161, pp. 217\u2013232. Springer, Heidelberg (2013)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-24749-1_7","volume-title":"Computer Performance Engineering","author":"F. Ghassemi","year":"2011","unstructured":"Ghassemi, F., Talebi, M., Movaghar, A., Fokkink, W.: Stochastic restricted broadcast process theory. In: Thomas, N. (ed.) EPEW 2011. LNCS, vol.\u00a06977, pp. 72\u201386. Springer, Heidelberg (2011)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-68863-1_10","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"M. Katelman","year":"2008","unstructured":"Katelman, M., Meseguer, J., Hou, J.: Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 150\u2013169. Springer, Heidelberg (2008)"},{"issue":"2-3","key":"16_CR11","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/S0167-6423(96)00024-X","volume":"28","author":"P. Kosiuczenko","year":"1997","unstructured":"Kosiuczenko, P., Wirsing, M.: Timed rewriting logic with an application to object-based specification. Science of Computer Programming\u00a028(2-3), 225\u2013246 (1997)","journal-title":"Science of Computer Programming"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-21461-5_14","volume-title":"Formal Techniques for Distributed Systems","author":"D. Kouzapas","year":"2011","unstructured":"Kouzapas, D., Philippou, A.: A process calculus for dynamic networks. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol.\u00a06722, pp. 213\u2013227. Springer, Heidelberg (2011)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-319-12904-4_9","volume-title":"Rewriting Logic and Its Applications","author":"S. Liu","year":"2014","unstructured":"Liu, S., \u00d6lveczky, P.C., Meseguer, J.: A framework for mobile ad hoc networks in real-time maude. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol.\u00a08663, pp. 162\u2013177. Springer, Heidelberg (2014)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Meseguer, J.: Formal analysis of leader election in MANETs using Real-Time Maude (2014), \n \n http:\/\/www.ifi.uio.no\/RealTimeMaude\/leader-election-report.pdf","DOI":"10.1007\/978-3-319-15545-6_16"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Meseguer, J.: Modeling and analyzing mobile ad hoc networks in Real-Time Maude (submitted for publication, 2014), \n \n http:\/\/www.ifi.uio.no\/RealTimeMaude\/manets-report.pdf","DOI":"10.1007\/978-3-319-12904-4_9"},{"issue":"5","key":"16_CR16","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1007\/s00165-011-0210-7","volume":"25","author":"M. Merro","year":"2013","unstructured":"Merro, M., Sibilio, E.: A calculus of trustworthy ad hoc networks. Formal Aspects of Computing\u00a025(5), 801\u2013832 (2013)","journal-title":"Formal Aspects of Computing"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/978-3-319-12904-4_3","volume-title":"Rewriting Logic and Its Applications","author":"P.C. \u00d6lveczky","year":"2014","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol.\u00a08663, pp. 42\u201379. Springer, Heidelberg (2014)"},{"issue":"1-2","key":"16_CR18","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"P.C. \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-order and Symbolic Computation\u00a020(1-2), 161\u2013196 (2007)","journal-title":"Higher-order and Symbolic Computation"},{"key":"16_CR19","unstructured":"\u00d6lveczky, P.C.: Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic. Ph.D. thesis, University of Bergen, Norway (2000), \n \n http:\/\/maude.csl.sri.com\/papers"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Kosiuczenko, P., Wirsing, M.: An object-oriented algebraic steam-boiler control specification. In: Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.) Formal Methods for Industrial Applications. LNCS, vol.\u00a01165, pp. 379\u2013402. Springer, Heidelberg (1996)","DOI":"10.1007\/BFb0027246"},{"key":"16_CR21","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/S0304-3975(01)00363-2","volume":"285","author":"P.C. \u00d6lveczky","year":"2002","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science\u00a0285, 359\u2013405 (2002)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"16_CR22","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2007.06.005","volume":"176","author":"P.C. \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and completeness for Real-Time Maude. Electronic Notes in Theoretical Computer Science\u00a0176(4), 5\u201327 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"3","key":"16_CR23","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10703-006-0015-0","volume":"29","author":"P.C. \u00d6lveczky","year":"2006","unstructured":"\u00d6lveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER\/NCA active network protocol suite in Real-Time Maude. Formal Methods in System Design\u00a029(3), 253\u2013293 (2006)","journal-title":"Formal Methods in System Design"},{"issue":"2-3","key":"16_CR24","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/j.tcs.2008.09.022","volume":"410","author":"P.C. \u00d6lveczky","year":"2009","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theoretical Computer Science\u00a0410(2-3), 254\u2013280 (2009)","journal-title":"Theoretical Computer Science"},{"key":"16_CR25","unstructured":"OMNeT++., \n \n http:\/\/www.omnetpp.org\/\n \n \n (accessed November 24, 2014)"},{"key":"16_CR26","unstructured":"Sibilio, E.: Formal methods for wireless systems. Ph.D. Thesis, University of Verona (2011)"},{"issue":"6","key":"16_CR27","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1016\/j.scico.2009.07.008","volume":"75","author":"A. Singh","year":"2010","unstructured":"Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. Science of Computer Programming\u00a075(6), 440\u2013469 (2010)","journal-title":"Science of Computer Programming"},{"key":"16_CR28","unstructured":"Song, L.: Probabilistic models and process calculi for mobile ad hoc networks. Ph.D. Thesis, IT University of Copenhagen (2012)"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-642-33475-7_24","volume-title":"Theoretical Computer Science","author":"L. Song","year":"2012","unstructured":"Song, L., Godskesen, J.C.: Broadcast abstraction in a stochastic calculus for mobile networks. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol.\u00a07604, pp. 342\u2013356. Springer, Heidelberg (2012)"},{"key":"16_CR30","unstructured":"Su, P.: Delay measurement time synchronization for wireless sensor networks. Tech. Rep. IRB-TR-03-013, Intel Research Berkeley Lab (2003)"},{"key":"16_CR31","unstructured":"Vasudevan, S., Kurose, J.F., Towsley, D.F.: Design and analysis of a leader election algorithm for mobile ad hoc networks. Tech. Rep. UMass CMPSCI 03-20, University of Massachusetts (2003)"},{"key":"16_CR32","unstructured":"Vasudevan, S., Kurose, J.F., Towsley, D.F.: Design and analysis of a leader election algorithm for mobile ad hoc networks. In: Proc. ICNP 2004. IEEE (2004)"}],"container-title":["Lecture Notes in Computer Science","Software, Services, and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15545-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T13:46:42Z","timestamp":1559137602000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-15545-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319155449","9783319155456"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15545-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}