{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,24]],"date-time":"2024-08-24T21:18:01Z","timestamp":1724534281098},"reference-count":25,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/501100004329","name":"Slovenian Research Agency","doi-asserted-by":"publisher","award":["P2-0069"],"id":[{"id":"10.13039\/501100004329","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Simulation Modelling Practice and Theory"],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1016\/j.simpat.2017.08.002","type":"journal-article","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T18:15:31Z","timestamp":1502216131000},"page":"367-378","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":8,"special_numbering":"C","title":["Using PRISM model checker as a validation tool for an analytical model of IEEE 802.15.4 networks"],"prefix":"10.1016","volume":"77","author":[{"given":"Tatjana","family":"Kapus","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.simpat.2017.08.002_bib0001","doi-asserted-by":"crossref","first-page":"3480","DOI":"10.1109\/TVT.2009.2014956","article-title":"Performance analysis of IEEE 802.15.4 non beacon-enabled mode","volume":"58","author":"Buratti","year":"2009","journal-title":"IEEE Trans. Veh. Technol."},{"key":"10.1016\/j.simpat.2017.08.002_bib0002","series-title":"Sensor Networks with IEEE 802.15.4 Systems","first-page":"161","article-title":"Performance analysis of the IEEE 802.15.4 MAC protocol","author":"Buratti","year":"2011"},{"key":"10.1016\/j.simpat.2017.08.002_bib0003","unstructured":"G. Norman, D. Parker, Quantitative verification: Formal guarantees for timeliness, reliability and performance, a Knowledge Transfer Report from the London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering, 2014."},{"key":"10.1016\/j.simpat.2017.08.002_bib0004","series-title":"Proc. 2nd IFIP\/IEEE Int. Symp. Theoretical Aspects of Software Engineering (TASE)","first-page":"3","article-title":"Perspectives in probabilistic verification","author":"Katoen","year":"2008"},{"key":"10.1016\/j.simpat.2017.08.002_bib0005","series-title":"Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, ISTE Ltd.","first-page":"249","article-title":"Verification of real-time probabilistic systems","author":"Kwiatkowska","year":"2008"},{"key":"10.1016\/j.simpat.2017.08.002_bib0006","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1145\/1530873.1530882","article-title":"PRISM: probabilistic model checking for performance and reliability analysis","volume":"36","author":"Kwiatkowska","year":"2009","journal-title":"Perf. E. R."},{"key":"10.1016\/j.simpat.2017.08.002_bib0007","unstructured":"OMNeT++ Simulation Manual, https:\/\/omnetpp.org\/doc\/omnetpp\/manual\/ accessed 19.07.2017."},{"key":"10.1016\/j.simpat.2017.08.002_bib0008","unstructured":"OPNET: Manual de usuario, Universitat Polit\u00e8cnica de Catalunya, Departament d\u2019Enginyeria Telem\u00e0tica, Secci\u00f3 de l\u2019EPSEVG, Sept. 2004."},{"key":"10.1016\/j.simpat.2017.08.002_bib0009","series-title":"Proc. 1st Int. Conf. Runtime Verification (RV)","first-page":"122","article-title":"Statistical model checking: An overview","author":"Legay","year":"2010"},{"key":"10.1016\/j.simpat.2017.08.002_bib0010","series-title":"Proc. 2nd Joint Int. Workshop Process Algebra and Probabilistic Methods and Performance Modeling in Verification (PAPMPROBMIV)","first-page":"169","article-title":"Probabilistic model checking of the IEEE 802.11 wireless local area network protocols","author":"Kwiatkowska","year":"2002"},{"key":"10.1016\/j.simpat.2017.08.002_bib0011","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/s10009-003-0118-5","article-title":"Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM","volume":"5","author":"Daws","year":"2004","journal-title":"Int. J. Soft. Tools Technol. Transfer"},{"key":"10.1016\/j.simpat.2017.08.002_bib0012","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/j.entcs.2005.04.012","article-title":"Probabilistic model checking of the CSMA\/CD protocol using PRISM and APMC","volume":"128","author":"Duflot","year":"2005","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.simpat.2017.08.002_bib0013","series-title":"Proc. 5th Int. Workshop Automated Specification and Verification of Web Systems","article-title":"Analyzing a proxy cache server performance model with the probabilistic model checker PRISM","author":"B\u00e9rczes","year":"2009"},{"key":"10.1016\/j.simpat.2017.08.002_bib0014","series-title":"Proc. 23rd Int. Conf. Computer Aided Verification (CAV 2011)","first-page":"585","article-title":"PRISM 4.0: verification of probabilistic real-time systems","author":"Kwiatkowska","year":"2011"},{"key":"10.1016\/j.simpat.2017.08.002_bib0015","series-title":"Proc. 6th Int. Conf. Quantitative Evaluation of Systems","first-page":"41","article-title":"On the impact of modelling choices for distributed information spread","author":"Bakhshi","year":"2009"},{"key":"10.1016\/j.simpat.2017.08.002_bib0016","unstructured":"PRISM Manual, http:\/\/www.prismmodelchecker.org\/manual\/ accessed 12.01.2017."},{"key":"10.1016\/j.simpat.2017.08.002_bib0017","series-title":"Proc. 2nd Int. Symp. Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)","first-page":"290","article-title":"Probabilistic model checking of contention resolution in the IEEE 802.15.4 low-rate wireless personal area network protocol","author":"Fruth","year":"2006"},{"key":"10.1016\/j.simpat.2017.08.002_bib0018","series-title":"Formal methods for the analysis of wireless network protocols, Ph.D. thesis","author":"Fruth","year":"2011"},{"key":"10.1016\/j.simpat.2017.08.002_bib0019","first-page":"157","article-title":"Modelling medium access control in IEEE 802.15.4 nonbeacon-enabled networks with probabilistic timed automata","volume":"9","author":"Kapus","year":"2013","journal-title":"Mob. Inf. Syst."},{"key":"10.1016\/j.simpat.2017.08.002_bib0020","unstructured":"Part 15.4: Wireless medium access control (MAC) and physical layer (PHY) specifications for low-rate wireless personal area networks (WPANs), IEEE Std 802.15.4-2006."},{"key":"10.1016\/j.simpat.2017.08.002_bib0021","series-title":"Proc. 23rd Telecommunications Forum (TELFOR 2015)","first-page":"87","article-title":"Analysing the effect of CCA duration in 802.15.4 networks with hidden nodes by using PRISM","author":"Kapus","year":"2015"},{"key":"10.1016\/j.simpat.2017.08.002_bib0022","doi-asserted-by":"crossref","first-page":"3191","DOI":"10.1109\/TVT.2012.2201221","article-title":"Analytical modeling of multi-hop IEEE 802.15.4 networks","volume":"61","author":"Marco","year":"2012","journal-title":"IEEE Trans. Veh. Technol."},{"key":"10.1016\/j.simpat.2017.08.002_bib0023","series-title":"Proc. 2010 Mini-Conf. Applied Theoretical Computer Science (MATCOS-10)","first-page":"121","article-title":"Model checking of the slotted CSMA\/CA MAC protocol of the IEEE 802.15.4 standard","author":"N\u00e9meth","year":"2011"},{"key":"10.1016\/j.simpat.2017.08.002_bib0024","series-title":"Formal Methods for Industrial Critical Systems: A Survey of Applications","first-page":"133","article-title":"Practical applications of probabilistic model checking to communication protocols","author":"Duflot","year":"2012"},{"key":"10.1016\/j.simpat.2017.08.002_bib0025","series-title":"MEng final year project dissertation","article-title":"Software project m60: Simulator for the probabilistic model checker PRISM","author":"Hinton","year":"2005"}],"container-title":["Simulation Modelling Practice and Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1569190X17301119?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1569190X17301119?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,8,28]],"date-time":"2018-08-28T13:31:23Z","timestamp":1535463083000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1569190X17301119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":25,"alternative-id":["S1569190X17301119"],"URL":"https:\/\/doi.org\/10.1016\/j.simpat.2017.08.002","relation":{},"ISSN":["1569-190X"],"issn-type":[{"value":"1569-190X","type":"print"}],"subject":[],"published":{"date-parts":[[2017,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Using PRISM model checker as a validation tool for an analytical model of IEEE 802.15.4 networks","name":"articletitle","label":"Article Title"},{"value":"Simulation Modelling Practice and Theory","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.simpat.2017.08.002","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2017 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}