{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:52Z","timestamp":1761597052263},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418634"},{"type":"electronic","value":"9783540453147"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45314-8_24","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T12:01:23Z","timestamp":1194955283000},"page":"333-347","source":"Crossref","is-referenced-by-count":12,"title":["Specification and Analysis of the AER\/NCA Active Network Protocol Suite in Real-Time Maude"],"prefix":"10.1007","author":[{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"first","affiliation":[]},{"given":"Mark","family":"Keaton","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Zabele","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"24_CR1","unstructured":"Active error recovery (AER): AER\/NCA software release version 1.1. http:\/\/www.tascnets.com\/panama\/AER\/ , May 2000."},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","volume-title":"A Decade of Concurrency-Reflections and Perspectives","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and D. Long. Verification tools for-nite-state concurrent systems. In A Decade of Concurrency-Reflections and Perspectives, volume 803 of Lecture Notes in Computer Science. Springer, 1994."},{"key":"24_CR3","volume-title":"Maude: Specification and Programming in Rewriting Logic","author":"M. Clavel","year":"1999","unstructured":"M. Clavel, F. Dur\u00e1n, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, and J. Quesada. Maude: Specification and Programming in Rewriting Logic. Computer Science Laboratory, SRI International, Menlo Park, 1999. http:\/\/maude.csl.sri.com ."},{"key":"24_CR4","unstructured":"G. Denker, J. Meseguer, and C. L. Talcott. Formal specification and analysis of active networks and communication protocols: The Maude experience. In DARPA Information Survivability Conference and Exposition (DISCEX 2000). IEEE, 2000."},{"key":"24_CR5","unstructured":"F. Dur\u00e1n. A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, University of M\u00e1laga, 1999."},{"key":"24_CR6","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"issue":"5","key":"24_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"24_CR8","unstructured":"S. Kasera, S. Bhattacharyya, M. Keaton, D. Kiwior, J. Kurose, D. Towsley, and S. Zabele. Scalable fair reliable multicast using active services. Technical Report TR 99-44, University of Massachusetts, Amherst, CMPSCI, 1999."},{"issue":"1-2","key":"24_CR9","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1-2):134\u2013152, October 1997. See also Uppaal home-page at http:\/\/www.uppaal.com\/ .","journal-title":"Software Tools for Technology Transfer"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96:73\u2013155, 1992.","journal-title":"Theoretical Computer Science"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"J. Meseguer. Rewriting logic and Maude: a wide-spectrum semantic framework for object-based distributed systems. In S. Smith and C.L. Talcott, editors, Formal Methods for Open Object-based Distributed Systems, FMOODS 2000, pages 89\u2013117. Kluwer, 2000.","DOI":"10.1007\/978-0-387-35520-7_5"},{"key":"24_CR12","unstructured":"P. C. \u00d6lveczky. Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic. PhD thesis, University of Bergen, 2000. Available at http:\/\/maude.csl.sri.com\/papers ."},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"P. C. \u00d6lveczky. Specifying and analyzing the AER\/NCA active network protocols in Real-Time Maude. http:\/\/www.csl.sri.com\/~peter\/AER\/AER.html , 2000.","DOI":"10.1007\/3-540-45314-8_24"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"P. C. \u00d6lveczky and J. Meseguer. Real-Time Maude: A tool for simulating and analyzing real-time and hybrid systems. In Third International Workshop on Rewriting Logic and its Applications, 2000. To appear in Electronic Notes in Theoretical Computer Science.","DOI":"10.1016\/S1571-0661(05)80134-3"},{"key":"24_CR15","unstructured":"P. C. \u00d6lveczky and J. Meseguer. Specification of real-time and hybrid systems in rewriting logic. To appear in Theoretical Computer Science. Available at http:\/\/maude.csl.sri.com\/papers , September 2000."},{"key":"24_CR16","first-page":"748","volume":"607","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In Automated Deduction-CADE-11, volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752, 1992.","journal-title":"Automated Deduction-CADE-11"},{"key":"24_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle, volume 828 of Lecture Notes in Computer Science. Springer Verlag, 1994."},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"S. Yovine. Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer, 1(1\/2), 1997. See also Kronos home-page at http:\/\/www-verimag.imag.fr\/TEMPORISE\/kronos\/ .","DOI":"10.1007\/s100090050009"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45314-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T14:01:17Z","timestamp":1684072877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45314-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418634","9783540453147"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45314-8_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}