{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:40:13Z","timestamp":1771026013868,"version":"3.50.1"},"reference-count":16,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,5]]},"DOI":"10.1109\/vetecs.2011.5956327","type":"proceedings-article","created":{"date-parts":[[2011,7,21]],"date-time":"2011-07-21T11:16:25Z","timestamp":1311246985000},"page":"1-5","source":"Crossref","is-referenced-by-count":22,"title":["Formal Analysis of a VANET Congestion Control Protocol through Probabilistic Verification"],"prefix":"10.1109","author":[{"given":"Savas","family":"Konur","sequence":"first","affiliation":[]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","year":"2007","journal-title":"IEEE P802 11p\/D0 21 Draft Amendment for Wireless Access in Vehicular Environments (WAVE)"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2004.1354670"},{"key":"ref12","first-page":"113","article-title":"PRISM: Probabilistic Symbolic Model Checker","volume":"2324","author":"kwiatkowska","year":"2002","journal-title":"Comp Perf Eval Modelling Techniques & Tools"},{"key":"ref13","doi-asserted-by":"crossref","first-page":"77","DOI":"10.3233\/FI-2010-298","article-title":"Model Checking Optimisation Based Congestion Control Models","volume":"102","author":"lomuscio","year":"2010","journal-title":"Fundamenta Infor-maticae"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1080754.1080762"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/ICVES.2005.1563614"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ITST.2006.289012"},{"key":"ref4","first-page":"241","article-title":"NuSMV 2: An OpenSource Tool for Symbolic Model Checking","author":"cimatti","year":"2002","journal-title":"Proc Conf Computer Aided Verification"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/ICUMT.2009.5345640"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"ref5","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref8","first-page":"441","article-title":"PRISM: A Tool for Automatic Verification of Probabilistic Systems","author":"hinton","year":"2006","journal-title":"Proc 12th TACAS"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref2","first-page":"526","article-title":"A Cooperative and Fully-distributed Congestion Control Approach within VANETs","author":"bouassida","year":"2009","journal-title":"Proc 9th ITST"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/BFb0020949","article-title":"UPPAAL-A Tool Suite for Automatic Verification of Real-time Sys-tems","author":"bengtsson","year":"1996","journal-title":"Proc of the DIMACS International Workshop on Verification and Control of Hybrid Systems"},{"key":"ref9","author":"holzmann","year":"1991","journal-title":"Design and Validation of Computer Protocols"}],"event":{"name":"2011 IEEE Vehicular Technology Conference (VTC 2011-Spring)","location":"Budapest, Hungary","start":{"date-parts":[[2011,5,15]]},"end":{"date-parts":[[2011,5,18]]}},"container-title":["2011 IEEE 73rd Vehicular Technology Conference (VTC Spring)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5954014\/5956103\/05956327.pdf?arnumber=5956327","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,21]],"date-time":"2020-06-21T09:37:23Z","timestamp":1592732243000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5956327\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5]]},"references-count":16,"URL":"https:\/\/doi.org\/10.1109\/vetecs.2011.5956327","relation":{},"subject":[],"published":{"date-parts":[[2011,5]]}}}