{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T04:02:31Z","timestamp":1725681751347},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1109\/pimrc.2010.5671736","type":"proceedings-article","created":{"date-parts":[[2010,12,22]],"date-time":"2010-12-22T01:36:16Z","timestamp":1292981776000},"page":"2471-2476","source":"Crossref","is-referenced-by-count":1,"title":["Using formal verification methods and tools for protocol profiling and performance assessment in mobile and wireless environments"],"prefix":"10.1109","author":[{"given":"Stylianos","family":"Georgoulas","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Moessner","sequence":"additional","affiliation":[]},{"given":"Bruce","family":"Mcaleer","sequence":"additional","affiliation":[]},{"given":"Rahim","family":"Tafazolli","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"journal-title":"MVCE Core 5 Green Radio Research Programme","year":"0","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1402958.1402985"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2008.93"},{"key":"ref15","article-title":"Dynamic configuration of IPv4 link-local addresses","author":"cheshire","year":"2005","journal-title":"Internet RFC"},{"journal-title":"BitTorrent website","year":"0","key":"ref16"},{"year":"1997","key":"ref17"},{"year":"2002","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0005-2"},{"journal-title":"Ns-2","year":"0","key":"ref28"},{"key":"ref4","doi-asserted-by":"crossref","DOI":"10.1007\/s10009-006-0014-x","article-title":"A formal analysis of bluetooth device discovery","author":"duflot","year":"2006","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"ref27","article-title":"Compositional reasoning in model checking","author":"berezin","year":"1997","journal-title":"COMPOSE*"},{"key":"ref3","article-title":"Practical applications of probabilistic model checking to communication protocols","author":"duflot","year":"2007","journal-title":"Handbook of Formal Methods in Industrial Critical Systems"},{"journal-title":"PRISM Website","year":"0","key":"ref6"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1481506.1481511"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275"},{"journal-title":"The PRISM manual available at the PRISM website","year":"0","key":"ref7"},{"key":"ref2","article-title":"Modeling and formal verification of DHCP using SPIN","author":"islam","year":"2006","journal-title":"International Journal of Computer Science and Applications"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2009.11"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/MASCOT.2000.876429"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1030194.1015508"},{"key":"ref21","article-title":"Analyzing and improving BitTorrent performance","author":"bharambe","year":"2005","journal-title":"Microsoft Research Tech Rep MSR-TR"},{"key":"ref24","article-title":"Probabilistic model checking of the IEEE 802.11 wireless local area network protocol","author":"kwiatkowska","year":"2002","journal-title":"PAPM\/PROBMIV"},{"key":"ref23","article-title":"Energy consumption in mobile peer-to-peer- quantitative results form file sharing","author":"nurminen","year":"2008","journal-title":"IEEE CCNC"},{"key":"ref26","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36577-X_24","article-title":"Learning assumptions for compositional verification","author":"cobleigh","year":"2003","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref25","article-title":"Symbolic model checking for probabilistic timed automata","author":"kwiatkowska","year":"2004","journal-title":"FORMATS\/FTRTFT"}],"event":{"name":"2010 IEEE 21st International Symposium on Personal, Indoor and Mobile Radio Communications - (PIMRC 2010)","start":{"date-parts":[[2010,9,26]]},"location":"Istanbul, Turkey","end":{"date-parts":[[2010,9,30]]}},"container-title":["21st Annual IEEE International Symposium on Personal, Indoor and Mobile Radio Communications"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5656620\/5671569\/05671736.pdf?arnumber=5671736","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T17:31:38Z","timestamp":1497893498000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5671736\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/pimrc.2010.5671736","relation":{},"subject":[],"published":{"date-parts":[[2010,9]]}}}