{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,9]],"date-time":"2023-10-09T14:58:05Z","timestamp":1696863485205},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2005,11,1]],"date-time":"2005-11-01T00:00:00Z","timestamp":1130803200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2005,11]]},"DOI":"10.1007\/s10703-005-3398-4","type":"journal-article","created":{"date-parts":[[2005,12,24]],"date-time":"2005-12-24T05:55:40Z","timestamp":1135403740000},"page":"213-251","source":"Crossref","is-referenced-by-count":2,"title":["Network Event Recognition"],"prefix":"10.1007","volume":"27","author":[{"given":"Karthikeyan","family":"Bhargavan","sequence":"first","affiliation":[]},{"given":"Carl A.","family":"Gunter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3398_CR1","unstructured":"K. Bhargavan, \u201cNetwork Event Recognition,\u201d Ph D thesis, University of Pennsylvania, 2003."},{"key":"3398_CR2","doi-asserted-by":"crossref","unstructured":"K. Bhargavan, C.A. Gunter, and D. Obradovic, \u201cFault origin adjudication,\u201d Formal Methods in Software Practice, 2000.","DOI":"10.1145\/349360.351132"},{"issue":"2","key":"3398_CR3","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1109\/32.988495","volume":"28","author":"K. Bhargavan","year":"2002","unstructured":"K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, and M. Viswanathan, \u201cVerisim: Formal analysis of network simulations,\u201d IEEE Transactions on Software Engineering, Vol. 28, No. 2, pp. 129\u2013145, 2002.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3398_CR4","doi-asserted-by":"crossref","unstructured":"K. Bhargavan, S. Chandra, P.J. McCann, and C. A Gunter, \u201cWhat packets may come: Automata for network monitoring,\u201din Proceedings of the Symposium on Principles of Programming Languages (POPL'01), ACM Press, pp. 206\u2013219, 2001.","DOI":"10.1145\/360204.360221"},{"key":"3398_CR5","doi-asserted-by":"crossref","unstructured":"D. Binkley and K. Brian Gallagher, \u201cProgram slicing,\u201d Advances in Computers, 1996.","DOI":"10.1016\/S0065-2458(08)60641-5"},{"key":"3398_CR6","unstructured":"G.V. Bochmann and O. Bellal, \u201cTest result analysis with respect to formal specifications,\u201d in Proc. 2-nd Int. Workshop on Protocol Test Systems. Berlin, 1989 pp. 272\u2013294,."},{"key":"3398_CR7","doi-asserted-by":"crossref","unstructured":"R. Braden, \u201cRequirements for internet hosts\u2014communication layers,\u201d Technical Report RFC 1122, IETF, 1989.","DOI":"10.17487\/rfc1122"},{"key":"3398_CR8","doi-asserted-by":"crossref","unstructured":"M. Crispin, \u201cInternet message access protocol\u2014Version 4rev1,\u201dTechnical Report RFC 2060, IETF, 1996.","DOI":"10.17487\/rfc2060"},{"key":"3398_CR9","doi-asserted-by":"crossref","unstructured":"D. Crocker, \u201cStandard for the format of ARPA internet text messages,\u201d Technical Report RFC 822, IETF, 1982.","DOI":"10.17487\/rfc0822"},{"key":"3398_CR10","doi-asserted-by":"crossref","unstructured":"S.A. Ezust and G.V. Bochmann, \u201cAn automatic trace analysis tool generator for estelle specifications,\u201d Computer Communication Review, Vol. 25, No. 4, pp. 175\u2013184, 1995 Proceedings of ACM SIGCOMM 95 Conference.","DOI":"10.1145\/217382.217428"},{"key":"3398_CR11","unstructured":"D.J. Farber and J.B. Picken, The overseer, a powerful communications attribute for debugging and security in thin-wire connected control structures, in Proceedings of International Computer Communications Conference, 1976."},{"key":"3398_CR12","unstructured":"G.J. Holzmann, \u201cSPIN-formal verification,\u201d Web Page. Available at http:\/\/netlib.bell-labs.com\/netlib\/spin\/whatispin.html."},{"key":"3398_CR13","unstructured":"G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991. http:\/\/cm.bell-labs.com\/cm\/cs\/what\/spin\/Doc\/Book91.html."},{"key":"3398_CR14","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann, Logic Verification of ANSI-C Code with SPIN, Springer Verlag\/LNCS, 1885, pp. 131\u2013147, 2000.","DOI":"10.1007\/10722468_8"},{"key":"3398_CR15","unstructured":"IPInformation Sciences Institute, \u201cInternet protocol,\u201d Technical Report RFC 791, IETF, 1981a."},{"key":"3398_CR16","unstructured":"TCPInformation Sciences Institute, \u201cTransmission control protocol,\u201d Technical Report RFC 793, IETF, 1981b."},{"key":"3398_CR17","doi-asserted-by":"crossref","unstructured":"J. Klensin, \u201cSimple mail transfer protocol,\u201d Technical Report RFC 2821, IETF, 2001.","DOI":"10.17487\/rfc2821"},{"key":"3398_CR18","doi-asserted-by":"crossref","unstructured":"E. Kohler, M. Frans Kaashoek, and D.R. Montgomery, \u201cA readable TCP in the Prolac protocol language,\u201d in Proceedings of the ACM SIGCOMM'99 Conference: Applications, Technologies, Architectures, and Protocols for Computer Communication, Cambridge, Massachusetts, pp. 3\u201313, 1999.","DOI":"10.1145\/316188.316200"},{"key":"3398_CR19","unstructured":"I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan, \u201cRuntime assurance based on formal specifications,\u201d in Proceedings International Conference on Parallel and Distributed Processing Techniques and Applications, 1999."},{"key":"3398_CR20","unstructured":"Lotos: A formal description technique, 1987."},{"key":"3398_CR21","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"3398_CR22","doi-asserted-by":"crossref","unstructured":"P. McCann and S. Chandra, \u201cPacket Types: Abstract specification of network protocol messages,\u201d in ACM Conference of Special Interest Group on Data Communications (SIGCOMM), August 2000.","DOI":"10.1145\/347059.347563"},{"key":"3398_CR23","doi-asserted-by":"crossref","unstructured":"J. Myers and M. Rose, \u201cPost Office Protocol\u2014Version 3.\u201d Technical Report RFC 1939, IETF, 1996.","DOI":"10.17487\/rfc1939"},{"key":"3398_CR24","doi-asserted-by":"crossref","unstructured":"NSS Group, \u201cIntrusion detection systems\u2014group test,\u201d December 2001.","DOI":"10.1016\/S1361-3723(01)00614-5"},{"key":"3398_CR25","doi-asserted-by":"crossref","unstructured":"V. Paxson, \u201cAutomated packet trace analysis of TCP implementations,\u201d in ACM SIGCOMM'97, September 1997.","DOI":"10.1145\/263105.263160"},{"key":"3398_CR26","doi-asserted-by":"crossref","first-page":"2435","DOI":"10.1016\/S1389-1286(99)00112-7","volume":"31","author":"V. Paxson","year":"14 December 1999","unstructured":"V. Paxson, \u201cBro: A system for detecting network intruders in real-time,\u201d Computer Networks, Vol. 31, pp. 2435\u20132463, 14 December 1999.This paper is a revision of paper that previously appeared in Proc. 7th USENIX Security Symposium, January 1998.","journal-title":"Computer Networks"},{"key":"3398_CR27","unstructured":"C. Perkins, \u201cAd hoc on-demand distance vector (AODV) routing,\u201d Internet-Draft Version 00, IETF, 1997."},{"key":"3398_CR28","doi-asserted-by":"crossref","unstructured":"C.E. Perkins and E.M. Royer, \u201cAd-hoc on-demand distance vector routing,\u201d in Proceedings of the 2nd IEEE Workshop on Mobile Computer Systems and Applications, 1999, pp. 90\u2013100.","DOI":"10.1109\/MCSA.1999.749281"},{"key":"3398_CR29","doi-asserted-by":"crossref","unstructured":"J. Postel, \u201cInternet control message protocol,\u201d Technical Report RFC 792, IETF, 1981.","DOI":"10.17487\/rfc0777"},{"key":"3398_CR30","doi-asserted-by":"crossref","unstructured":"J.B. Postel, \u201cSimple mail transfer protocol,\u201d Technical Report RFC 821, IETF, 1982.","DOI":"10.17487\/rfc0821"},{"key":"3398_CR31","unstructured":"T.H. Ptacek and T.N. Newsham, \u201cInsertion, evasion and denial of service: Eluding network intrusion detection,\u201d Technical report, Secure Networks, Inc., 1998."},{"key":"3398_CR32","doi-asserted-by":"crossref","unstructured":"P. Resnick, \u201cInternet message format,\u201d Technical Report RFC 2822, IETF, 2001.","DOI":"10.17487\/rfc2822"},{"key":"3398_CR33","volume-title":"The Protocols","author":"W.R. Stevens","year":"1994","unstructured":"W.R. Stevens, \u201cTCP\/IP Illustrated, Volume 1, The Protocols,\u201dAddison-Wesley, Reading, Massachusetts, Vol. 1, 1994."},{"key":"3398_CR34","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"F. Tip, \u201cA survey of program slicing techniques,\u201d Journal of Programming Languages, Vol. 3, pp. 121\u2013189, 1995.","journal-title":"Journal of Programming Languages"},{"issue":"9","key":"3398_CR35","doi-asserted-by":"crossref","first-page":"963","DOI":"10.1002\/(SICI)1097-024X(19980725)28:9<963::AID-SPE179>3.0.CO;2-9","volume":"28","author":"R. Renesse van","year":"1998","unstructured":"R. van Renesse, K. Birman, M. Hayden, A. Vaysburd, and D. Karr, \u201cBuilding adaptive systems using Ensemble,\u201d Softw. Pract. Exper., Vol. 28, No. 9, pp. 963\u2013979, 1998.","journal-title":"Softw. Pract. Exper."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-3398-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-005-3398-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-3398-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T20:15:51Z","timestamp":1586636151000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-005-3398-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,11]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,11]]}},"alternative-id":["3398"],"URL":"https:\/\/doi.org\/10.1007\/s10703-005-3398-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,11]]}}}