{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T14:04:13Z","timestamp":1773324253321,"version":"3.50.1"},"reference-count":21,"publisher":"SAGE Publications","issue":"5","license":[{"start":{"date-parts":[[2015,5,1]],"date-time":"2015-05-01T00:00:00Z","timestamp":1430438400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"funder":[{"DOI":"10.13039\/501100007273","name":"Comisi\u00f3n Interministerial de Ciencia y Tecnolog\u00eda","doi-asserted-by":"crossref","award":["TIN2012-36812-C02-02."],"award-info":[{"award-number":["TIN2012-36812-C02-02."]}],"id":[{"id":"10.13039\/501100007273","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["International Journal of Distributed Sensor Networks"],"published-print":{"date-parts":[[2015,5,1]]},"abstract":"<jats:p> A novel collision resolution algorithm for wireless sensor networks is formally analysed via probabilistic model checking. The algorithm called 2CS-WSN is specifically designed to be used during the contention phase of IEEE 802.15.4. Discrete time Markov chains (DTMCs) have been proposed as modelling formalism and the well-known probabilistic symbolic model checker PRISM is used to check some correctness properties and different operating modes and, furthermore, to collect some performance measures. Thus, all the benefits of formal verification and simulation are gathered. These correctness properties as well as practical and relevant scenarios for the real world have agreed with the algorithm designers. <\/jats:p>","DOI":"10.1155\/2015\/285396","type":"journal-article","created":{"date-parts":[[2015,5,13]],"date-time":"2015-05-13T21:04:40Z","timestamp":1431551080000},"page":"285396","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":1,"title":["Probabilistic Model Checking: One Step Forward in Wireless Sensor Networks Simulation"],"prefix":"10.1177","volume":"11","author":[{"given":"Jos\u00e9 A.","family":"Mateo","sequence":"first","affiliation":[{"name":"Instituto de Investigaci\u00f3n en Inform\u00e1tica, Avenida de Espa\u00f1a s\/n. 02071 Albacete, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1462-5274","authenticated-orcid":false,"given":"Hermenegilda","family":"Maci\u00e0","sequence":"additional","affiliation":[{"name":"Instituto de Investigaci\u00f3n en Inform\u00e1tica, Avenida de Espa\u00f1a s\/n. 02071 Albacete, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2392-9272","authenticated-orcid":false,"given":"M. Carmen","family":"Ruiz","sequence":"additional","affiliation":[{"name":"Instituto de Investigaci\u00f3n en Inform\u00e1tica, Avenida de Espa\u00f1a s\/n. 02071 Albacete, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Calleja","sequence":"additional","affiliation":[{"name":"Instituto de Investigaci\u00f3n en Inform\u00e1tica, Avenida de Espa\u00f1a s\/n. 02071 Albacete, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fernando","family":"Royo","sequence":"additional","affiliation":[{"name":"Instituto de Investigaci\u00f3n en Inform\u00e1tica, Avenida de Espa\u00f1a s\/n. 02071 Albacete, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2015,5,13]]},"reference":[{"key":"B12-2015-285396","first-page":"183","volume-title":"Proceedings of the IEEE International Workshop on Factory Communication Systems (WFCS '06)","author":"Koubaa A."},{"key":"B17-2015-285396","first-page":"701","volume-title":"Proceedings of the Workshop on Energy-Efficient Wireless Communications and Networks (EWCN '04) Held in Conjunction with the IEEE International Performance Computing and Communications Conference (IPCCC '04)","author":"Lu G."},{"key":"B22-2015-285396","doi-asserted-by":"publisher","DOI":"10.1109\/GLOCOM.2009.5425742"},{"key":"B13-2015-285396","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV' 11)","volume":"6806","author":"Kwiatkowska M."},{"key":"B2-2015-285396","doi-asserted-by":"publisher","DOI":"10.1109\/49.840210"},{"key":"B24-2015-285396","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2002.1019408"},{"key":"B6-2015-285396","doi-asserted-by":"publisher","DOI":"10.1109\/TVT.2010.2063720"},{"key":"B16-2015-285396","doi-asserted-by":"publisher","DOI":"10.3390\/s100706275"},{"key":"B7-2015-285396","first-page":"253","volume-title":"Proceedings of the 6th International Conference on Integrated Formal Methods (IFM '07)","author":"Fehnker A."},{"key":"B15-2015-285396","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"B3-2015-285396","first-page":"1","volume-title":"Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages (QAPL '12)","author":"Bulychev P. E."},{"key":"B5-2015-285396","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.012"},{"key":"B9-2015-285396","first-page":"73","volume-title":"Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI '04)","author":"H\u00e9rault T."},{"key":"B14-2015-285396","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45605-8_11"},{"key":"B23-2015-285396","doi-asserted-by":"publisher","DOI":"10.1109\/ADCOM.2012.6563577"},{"key":"B18-2015-285396","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2013.05.433"},{"key":"B19-2015-285396","doi-asserted-by":"publisher","DOI":"10.1109\/18.42234"},{"key":"B21-2015-285396","series-title":"Wiley Series in Probability and Mathematical Statistics","volume-title":"Stochastic Processes","author":"Ross S. M.","year":"1983"},{"key":"B8-2015-285396","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"B4-2015-285396","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"B1-2015-285396","doi-asserted-by":"publisher","DOI":"10.1109\/SURV.2010.020510.00058"}],"container-title":["International Journal of Distributed Sensor Networks"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/journals.sagepub.com\/doi\/pdf\/10.1155\/2015\/285396","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/journals.sagepub.com\/doi\/full-xml\/10.1155\/2015\/285396","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/journals.sagepub.com\/doi\/pdf\/10.1155\/2015\/285396","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,5]],"date-time":"2021-05-05T21:45:28Z","timestamp":1620251128000},"score":1,"resource":{"primary":{"URL":"http:\/\/journals.sagepub.com\/doi\/10.1155\/2015\/285396"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,1]]},"references-count":21,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2015,5,1]]}},"alternative-id":["10.1155\/2015\/285396"],"URL":"https:\/\/doi.org\/10.1155\/2015\/285396","relation":{},"ISSN":["1550-1477","1550-1477"],"issn-type":[{"value":"1550-1477","type":"print"},{"value":"1550-1477","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,1]]}}}