{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T22:52:21Z","timestamp":1772751141893,"version":"3.50.1"},"reference-count":65,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Commun. Surv. Tutorials"],"published-print":{"date-parts":[[2002]]},"DOI":"10.1109\/comst.2002.5341329","type":"journal-article","created":{"date-parts":[[2009,12,8]],"date-time":"2009-12-08T19:38:50Z","timestamp":1260301130000},"page":"2-20","source":"Crossref","is-referenced-by-count":30,"title":["Formal methods for specification and analysis of communication protocols"],"prefix":"10.1109","volume":"4","author":[{"given":"Fulvio","family":"Babich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lia","family":"Deotto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","year":"2000","journal-title":"Final Draft International Standard 15437 Information technology Enhancements to LOTOS (E-LOTOS)"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"ref33","article-title":"Simulating Multicast Protocols in Estelle","author":"templemore-finlayson","year":"2000","journal-title":"Proc Int'l Conf FORTE\/PSTV'2000"},{"key":"ref32","year":"1993","journal-title":"Using Formal Description Techniques An Introduction to Estelle Lotos and SDL"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/ISCC.1997.615999"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.1999.776345"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/ICOIN.1998.648600"},{"key":"ref36","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1109\/ICPADS.2000.857686","article-title":"An Estelle-Based Probabilistic Partial Timed Protocol Verification System","author":"huang","year":"2000","journal-title":"Proc Int l Conf Parallel and Distributed Systems"},{"key":"ref1s","doi-asserted-by":"publisher","DOI":"10.1109\/32.508312"},{"key":"ref35","first-page":"117","article-title":"Using Formal Specification and Observers to Specify and Validate the ATM Signalinq Protocols","author":"atwood","year":"1999","journal-title":"Conf Local Computer Networks"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1016\/S0140-3664(99)00246-7"},{"key":"ref60","year":"2000","journal-title":"OMG Unified Modelinq Lanquage Specification"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/ICFEM.2000.873805"},{"key":"ref61","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/3-540-58468-4_163","article-title":"A Comparison of Statecharts Variants","volume":"863","author":"von der beeck","year":"1994","journal-title":"Lecture Notes in Computer Science"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/32.895987"},{"key":"ref28","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48234-2_19","article-title":"Embedding a Dialect of SDL in ProMeLa","author":"tuominen","year":"1999","journal-title":"Proc Theoretical and Practical Aspects of SPIN Model Checking 5th and 6th Int'l SPIN Wksps"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1049\/ic:19990007"},{"key":"ref27","author":"deotto","year":"2002","journal-title":"Formal Methods and Tools for Specification Validation and Performance Analysis of Communication Protocols of 2nd- and 3rd-Generation Mobile Systems"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.1998.665062"},{"key":"ref2","year":"0"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"ref20","year":"0"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_17"},{"key":"ref21","author":"holzmann","year":"1992","journal-title":"Description and Validation of Computer Protocols"},{"key":"ref24","article-title":"Slicing Promela and Its Applications to Protocol Understanding and Analysis","author":"millett","year":"1998","journal-title":"Proc 4th SPIN Wksp"},{"key":"ref23","article-title":"Extending Promela and Spin for Real Time","volume":"1055","author":"tripakis","year":"0","journal-title":"Proc TACAS '96 Lecture Notes in Computer Science"},{"key":"ref26","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/10722468_15","article-title":"Using Runtime Analysis to Guide Model Checking of Java Programs","volume":"1885","author":"havelund","year":"2000","journal-title":"Lecture Notes in Computer Science"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/10722468_8","article-title":"Logic Verification of ANSI C Code with SPIN","volume":"1885","author":"holzmann","year":"2000","journal-title":"Lecture Notes in Computer Science"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-5316(02)00102-5"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1016\/S0140-3664(99)00239-X"},{"key":"ref59","year":"1999","journal-title":"Recommendation Z 120 Message Sequence Chart (MSC)"},{"key":"ref58","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/BFb0035403","article-title":"The Bounded Retransmission Protocol Must Be On Time","volume":"1217","author":"d'argenio","year":"1997","journal-title":"Proc TACAS '97 Lecture Notes in Computer Science"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050032"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref55","first-page":"1997","article-title":"UPPAAL in a Nutshell","volume":"1+2","author":"larsen","year":"0","journal-title":"Springer International Journal of Software Tools for Technology Transfer"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050022"},{"key":"ref53","year":"0"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050021"},{"key":"ref10","year":"0"},{"key":"ref11","year":"0"},{"key":"ref40","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","article-title":"A Calculus of Communication Systems","author":"milner","year":"1980","journal-title":"Lecture Notes Computer Science"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/SBCCI.2000.876040"},{"key":"ref13","year":"0"},{"key":"ref14","year":"0"},{"key":"ref15","year":"0"},{"key":"ref16","article-title":"Compositional Verification of a Third-Generation Mobile Communication Protocol","author":"lepp\ufffdnen","year":"2000","journal-title":"Distributed System Validation and Verification DSVV '2000"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2000.896686"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/MELCON.2000.880372"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.1998.725410"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/52.391826"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/6.499951"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/2.375178"},{"key":"ref8","year":"0","journal-title":"Specification and Description Language (SDL)"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/5.533956"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/ICCIMA.1999.798551"},{"key":"ref9","author":"ellsberger","year":"1997","journal-title":"SDL Formal Object-Oriented Language for Communicating Systems"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-5316(99)00056-5"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/DCFTS.1999.814292"},{"key":"ref47","year":"1987","journal-title":"Protocol Specification Testing and Verification VII Elsevier Science\/North-Holland Publishers"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/WVL.1989.77040"},{"key":"ref41","author":"milner","year":"1989","journal-title":"Communication and Concurrency"},{"key":"ref44","article-title":"CADP'97 Status, Applications, and Perspectives","author":"garavel","year":"1997","journal-title":"Proc 2nd COST 247 Int'l Wksp Applied Formal Methods in System Design"},{"key":"ref43","first-page":"1232","article-title":"An Automatic Translation from Textual E-LOTOS into Graphic E-LOTOS","volume":"2","author":"yulan","year":"2000","journal-title":"Proc WCC-ICCT 2000"}],"container-title":["IEEE Communications Surveys & Tutorials"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9739\/5341328\/05341329.pdf?arnumber=5341329","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:17:42Z","timestamp":1638217062000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5341329\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"references-count":65,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/comst.2002.5341329","relation":{},"ISSN":["1553-877X"],"issn-type":[{"value":"1553-877X","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}