{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:54Z","timestamp":1740122694213,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T00:00:00Z","timestamp":1511740800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s10703-017-0309-4","type":"journal-article","created":{"date-parts":[[2017,11,27]],"date-time":"2017-11-27T11:07:43Z","timestamp":1511780863000},"page":"33-53","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Wireless protocol validation under uncertainty"],"prefix":"10.1007","volume":"53","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6516-9865","authenticated-orcid":false,"given":"Jinghao","family":"Shi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranveer","family":"Chandra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoffrey","family":"Challen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,27]]},"reference":[{"issue":"2","key":"309_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"309_CR2","doi-asserted-by":"crossref","unstructured":"Arnold M, Vechev M, Yahav E (2008) QVM: an efficient runtime for detecting defects in deployed systems. In: ACM SIGPLAN notices, vol 43. ACM, New York, pp 143\u2013162","DOI":"10.1145\/1449764.1449776"},{"key":"309_CR3","doi-asserted-by":"crossref","unstructured":"Bahl P, Chandra R, Padhye J, Ravindranath L, Singh M, Wolman A, Zill B (2006) Enhancing the security of corporate Wi-Fi networks using DAIR. In: Proceedings of the 4th international conference on mobile systems, applications and services. ACM, New York, pp 1\u201314","DOI":"10.1145\/1134680.1134682"},{"key":"309_CR4","unstructured":"Bartocci E, Grosu R, Karmarkar A, Smolka SA, Stoller SD, Zadok E, Seyster J (2012) Adaptive runtime verification. In: International conference on runtime verification. Springer, Berlin, pp 168\u2013182"},{"key":"309_CR5","unstructured":"Basin D, Klaedtke F, Marinovic S, Z\u0103linescu E (2012) Monitoring compliance policies over incomplete and disagreeing logs. In: International conference on runtime verification. Springer, Berlin, pp 151\u2013167"},{"key":"309_CR6","doi-asserted-by":"crossref","unstructured":"Bonakdarpour B, Navabpour S, Fischmeister S (2011) Sampling-based runtime verification. In: FM 2011: formal methods. Springer, Berlin, pp 88\u2013102","DOI":"10.1007\/978-3-642-21437-0_9"},{"issue":"1","key":"309_CR7","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/2654822.2541958","volume":"42","author":"J Bornholt","year":"2014","unstructured":"Bornholt J, Mytkowicz T, McKinley KS (2014) Uncertain $$<$$ < T $$>$$ > : a first-order type for uncertain data. ACM SIGARCH Comput Archit News 42(1):51\u201366","journal-title":"ACM SIGARCH Comput Archit News"},{"key":"309_CR8","volume-title":"Jigsaw: solving the puzzle of enterprise 802.11 analysis","author":"Y-C Cheng","year":"2006","unstructured":"Cheng Y-C, Bellardo J, Benk\u00f6 P, Snoeren AC, Voelker GM, Savage S (2006) Jigsaw: solving the puzzle of enterprise 802.11 analysis, vol 36. ACM, New York"},{"key":"309_CR9","unstructured":"Ciabarra M. WiFried: iOS 8 WiFi issue. https:\/\/goo.gl\/KtRDqk"},{"key":"309_CR10","doi-asserted-by":"crossref","unstructured":"Das A, Lahiri SK, Lal A, Li Y (2015) Angelic verification: precise verification modulo unknowns. In: Computer aided verification\u201427th international conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, proceedings, part I, pp 324\u2013342","DOI":"10.1007\/978-3-319-21690-4_19"},{"key":"309_CR11","unstructured":"digitalmediaphile. Windows 10 wifi issues with surface pro 3 and surface 3. http:\/\/goo.gl\/vBqiEo"},{"key":"309_CR12","unstructured":"Edelkamp S, Schuppan V, Bo\u0161na\u010dki D, Wijs A, Fehnker A, Aljazzar H (2008) Survey on directed model checking. In: International workshop on model checking and artificial intelligence. Springer, Berlin, pp 65\u201389"},{"key":"309_CR13","doi-asserted-by":"crossref","unstructured":"Elbaum S, Rosenblum DS (2014) Known unknowns: testing in the presence of uncertainty. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, FSE 2014, New York, NY, USA. ACM, pp 833\u2013836","DOI":"10.1145\/2635868.2666608"},{"key":"309_CR14","doi-asserted-by":"crossref","unstructured":"Fei L, Midkiff SP (2006) Artemis: practical runtime monitoring of applications for execution anomalies. In: ACM SIGPLAN notices, vol 41. ACM, New York, pp 84\u201395","DOI":"10.1145\/1133981.1133992"},{"key":"309_CR15","unstructured":"Gizmodo. The worst bugs in android 5.0 lollipop and how to fix them. http:\/\/goo.gl\/akDcvA"},{"key":"309_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid P (1997) Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, pp 174\u2013186","DOI":"10.1145\/263699.263717"},{"key":"309_CR17","unstructured":"Google. Google contact lens. https:\/\/en.wikipedia.org\/wiki\/Google_Contact_Lens"},{"key":"309_CR18","doi-asserted-by":"crossref","unstructured":"Hauswirth M, Chilimbi TM (2004) Low-overhead memory leak detection using adaptive statistical profiling. In: Acm SIGPLAN notices, vol 39. ACM, New York, pp 156\u2013164","DOI":"10.1145\/1024393.1024412"},{"key":"309_CR19","doi-asserted-by":"crossref","unstructured":"Jak\u0161i\u0107 S, Bartocci E, Grosu R, Ni\u010dkovi\u0107 D (2016) Quantitative monitoring of STL with edit distance. In: International conference on runtime verification. Springer, Berlin, pp 201\u2013218","DOI":"10.1007\/978-3-319-46982-9_13"},{"key":"309_CR20","doi-asserted-by":"crossref","unstructured":"Kalajdzic K, Bartocci E, Smolka SA, Stoller SD, Grosu R (2013) Runtime verification with particle filtering. In: International conference on runtime verification. Springer, Berlin, pp 149\u2013166","DOI":"10.1007\/978-3-642-40787-1_9"},{"issue":"3","key":"309_CR21","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1002\/bltj.2069","volume":"2","author":"A Kamerman","year":"1997","unstructured":"Kamerman A, Monteban L (1997) Wavelan\u00ae-II: a high-performance wireless lan for the unlicensed band. Bell Labs Tech J 2(3):118\u2013133","journal-title":"Bell Labs Tech J"},{"key":"309_CR22","doi-asserted-by":"crossref","unstructured":"Lacage M, Manshaei MH, Turletti T (2004) IEEE 802.11 rate adaptation: a practical approach. In: Proceedings of the 7th ACM international symposium on modeling, analysis and simulation of wireless and mobile systems. ACM, New York, pp 126\u2013134","DOI":"10.1145\/1023663.1023687"},{"key":"309_CR23","unstructured":"Lacage M, Manshaei MH, Turletti T (2004) IEEE 802.11 rate adaptation: a practical approach. Research report RR-5208 (<inria-00070784>), p 25"},{"key":"309_CR24","doi-asserted-by":"crossref","unstructured":"Lee D, Netravali AN, Sabnani KK, Sugla B, John A (1997) Passive testing and applications to network management. In: Proceedings, 1997 international conference on network protocols, 1997. IEEE, pp 113\u2013122","DOI":"10.1109\/ICNP.1997.643699"},{"key":"309_CR25","doi-asserted-by":"crossref","unstructured":"Mahajan R, Rodrig M, Wetherall D, Zahorjan J (2006) Analyzing the MAC-level behavior of wireless networks in the wild. In: ACM SIGCOMM computer communication review, vol 36. ACM, New York, pp 75\u201386","DOI":"10.1145\/1159913.1159923"},{"key":"309_CR26","doi-asserted-by":"crossref","unstructured":"Marino D, Musuvathi M, Narayanasamy S (2009) Literace: effective sampling for lightweight data-race detection. In: ACM Sigplan notices, vol 44. ACM, New York, pp 134\u2013143","DOI":"10.1145\/1542476.1542491"},{"issue":"SI","key":"309_CR27","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/844128.844136","volume":"36","author":"M Musuvathi","year":"2002","unstructured":"Musuvathi M, Park DY, Chou A, Engler DR, Dill DL (2002) CMC: a pragmatic approach to model checking real code. ACM SIGOPS Oper Syst Rev 36(SI):75\u201388","journal-title":"ACM SIGOPS Oper Syst Rev"},{"key":"309_CR28","unstructured":"Mytkowicz T, Sweeney PF, Hauswirth M, Diwan A (2008) Observer effect and measurement bias in performance analysis"},{"key":"309_CR29","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-642-12331-3_2","volume-title":"Modeling and tools for network simulation","author":"GF Riley","year":"2010","unstructured":"Riley GF, Henderson TR (2010) The ns-3 network simulator. In: Wehrle K, G\u00fcnes M, Gross J (eds) Modeling and tools for network simulation. Springer, Berlin, pp 15\u201334"},{"key":"309_CR30","doi-asserted-by":"crossref","unstructured":"Sampson A, Panchekha P, Mytkowicz T, McKinley KS, Grossman D, Ceze L (2014) Expressing and verifying probabilistic assertions. In: ACM SIGPLAN notices, vol 49. ACM, New York, pp 112\u2013122","DOI":"10.1145\/2666356.2594294"},{"key":"309_CR31","unstructured":"Savvius Inc. Savvius Wi-Fi adapters. https:\/\/goo.gl\/l3VXSx"},{"key":"309_CR32","first-page":"351","volume-title":"Wireless protocol validation under uncertainty","author":"J Shi","year":"2016","unstructured":"Shi J, Lahiri SK, Chandra R, Challen G (2016) Wireless protocol validation under uncertainty. Springer, Cham, pp 351\u2013367"},{"key":"309_CR33","unstructured":"Sistla AP, \u017defran M, Feng Y (2011) Runtime monitoring of stochastic cyber-physical systems with hybrid state. In: International conference on runtime verification. Springer, Berlin, pp 276\u2013293"},{"key":"309_CR34","first-page":"193","volume-title":"Runtime verification","author":"SD Stoller","year":"2011","unstructured":"Stoller SD, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka SA, Zadok E (2011) Runtime verification with state estimation. In: Khurshid S, Sen K (eds) Runtime verification. Springer, Berlin, pp 193\u2013207"},{"key":"309_CR35","unstructured":"Wikipedia. Chromecast. https:\/\/en.wikipedia.org\/wiki\/Chromecast"},{"key":"309_CR36","unstructured":"Wikipedia. Xbox one controller. https:\/\/en.wikipedia.org\/wiki\/Xbox_One_Controller"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0309-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0309-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0309-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,29]],"date-time":"2023-08-29T07:10:16Z","timestamp":1693293016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0309-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,27]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["309"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0309-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,11,27]]}}}