{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:26:50Z","timestamp":1777519610070,"version":"3.51.4"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2006,7,5]],"date-time":"2006-07-05T00:00:00Z","timestamp":1152057600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,10,27]]},"DOI":"10.1007\/s10009-006-0014-x","type":"journal-article","created":{"date-parts":[[2006,7,6]],"date-time":"2006-07-06T00:22:46Z","timestamp":1152145366000},"page":"621-632","source":"Crossref","is-referenced-by-count":72,"title":["A formal analysis of bluetooth device discovery"],"prefix":"10.1007","volume":"8","author":[{"given":"Marie","family":"Duflot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,7,5]]},"reference":[{"issue":"2\/3","key":"14_CR1","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"I. Bahar","year":"1997","unstructured":"Bahar I., Frohm E., Gaona C., Hachtel G., Macii E., Pardo A., Somenzi F. (1997) Algebraic decision diagrams and their applications. Form. Methods Syst. Des.10(2\/3): 171\u2013206","journal-title":"Form. Methods Syst. Des."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Basagni, S., Bruno, R., Petrioli, C.: Device discovery in Bluetooth networks: scatternet perspective. In: Proceedings of Networking 2002, LNCS, vol. 2345, pp. 1087\u20131092. Springer, Berlin Heidelberg NewYork (2002)","DOI":"10.1007\/3-540-47906-6_89"},{"key":"14_CR3","unstructured":"BlueHoc\u2014an open-source Bluetooth simulator.http:\/\/www-124.ibm.com\/developerworks\/opensource\/bluehoc"},{"key":"14_CR4","unstructured":"Bluetooth specification, version 1.2, Bluetooth SIG,http:\/\/www.bluetooth.com (2003)"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.: Binary decision diagrams and beyond: enabling technologies for formal verification. In: Proceedings of International Conference on Computer-Aided Design (ICCAD\u201995), pp. 236\u2013243 (1995)","DOI":"10.1109\/ICCAD.1995.480018"},{"issue":"2\/3","key":"14_CR6","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1023\/A:1008695706493","volume":"10","author":"E. Clarke","year":"1997","unstructured":"Clarke E., Fujita M., McGeer P., McMillan K., Yang J., Zhao X. (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form. Methods Syst. Des. 10(2\/3): 149\u2013169","journal-title":"Form. Methods Syst. Des."},{"issue":"2\u20133","key":"14_CR7","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/s10009-003-0118-5","volume":"5","author":"C. Daws","year":"2004","unstructured":"Daws C., Kwiatkowska M., Norman G. (2004) Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. Int. J. Softw. Tools Technol. Transf. 5(2\u20133): 221\u2013236","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Duflot, M., Fribourg, L., H\u00e9rault, T., Lassaigne, R., Magniette, F., Messika, S., Peyronnet, S., Picaronny, C.: Probabilistic model checking of the CSMA\/CD protocol using PRISM and APMC. In: Proceedings of the 4th Workshop on Automated Verification of Critical Systems (AVoCS\u201904). Electronic Notes in Theoretical Computer Science, vol. 128(6), pp. 195\u2013214. Elsevier, Amsterdam (2004)","DOI":"10.1016\/j.entcs.2005.04.012"},{"key":"14_CR9","unstructured":"Kasten, O., Langheinrich, M.: First experiences with Bluetooth in the Smart its distributed sensor network. In: Proceedings of PACT\u201901 (2001)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G.: Verifying randomized Byzantine agreement. In: Peled, D., Vardi, M. (eds.) Proceedings of Formal Techniques for Networked and Distributed Systems (FORTE\u201902). LNCS, vol. 2529, pp. 194\u2013209. Springer, Berlin Heidelberg NewYork (2002)","DOI":"10.1007\/3-540-36135-9_13"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Controller dependability analysis by probabilistic model checking. In: Proceedings of the 11th IFAC Symposium on Information Control Problems in Manufacturing (INCOM\u201904) (2004)","DOI":"10.1016\/S1474-6670(17)36115-3"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 2.0: a tool for probabilistic model checking. In: Proceedings of 1st International Conference on Quantitative Evaluation of Systems (QEST\u201904), pp. 322\u2013323. IEEE Computer Society Press, Los Alamites(2004)","DOI":"10.1109\/QEST.2004.1348048"},{"key":"14_CR13","first-page":"105","volume-title":"Proceedings Formal Modeling and Analysis of Timed Systems (FORMATS\u201903)","author":"M. Kwiatkowska","year":"2003","unstructured":"Kwiatkowska M., Norman G., Parker D., Sproston J. (2003). Performance analysis of probabilistic timed automata using digital clocks. In: Larsen K., Niebert P. (eds). Proceedings Formal Modeling and Analysis of Timed Systems (FORMATS\u201903). LNCS, vol. 2791, Springer, Berlin Heidelberg NewYork, pp. 105\u2013120"},{"key":"14_CR14","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Proceedings of 13th International Conference on Computer Aided Verification (CAV\u201901)","author":"M. Kwiatkowska","year":"2001","unstructured":"Kwiatkowska M., Norman G., Segala R. (2001). Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In: Berry G., Comon H., Finkel A. (eds). Proceedings of 13th International Conference on Computer Aided Verification (CAV\u201901). LNCS, vol. 2102, Springer, Berlin Heidelberg NewYork, pp. 194\u2013206"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) Proceedings of 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV\u201902). LNCS, vol. 2399, pp. 169\u2013187. Springer, Berlin Heidelberg NewYork (2002)","DOI":"10.1007\/3-540-45605-8_11"},{"issue":"3","key":"14_CR16","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"M. Kwiatkowska","year":"2003","unstructured":"Kwiatkowska M., Norman G., Sproston J. (2003) Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Form. Asp. Comput. 14(3): 295\u2013318","journal-title":"Form. Asp. Comput."},{"key":"14_CR17","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-3-540-30206-3_21","volume-title":"Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT)","author":"M. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska M., Norman G., Sproston J., Wang F. (2004). Symbolic model checking for probabilistic timed automata. In: Lakhnech Y., Yovine S. (eds). Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT). LNCS, vol. 3253, Springer,Berlin Heidelberg NewYork, pp. 293\u2013308"},{"issue":"10","key":"14_CR18","doi-asserted-by":"crossref","first-page":"1629","DOI":"10.1109\/TCAD.2005.852033","volume":"24","author":"G. Norman","year":"2005","unstructured":"Norman G., Parker D., Kwiatkowska M., Shukla S. (2005) Evaluating the reliability of NAND multiplexing with PRISM. IEEE Trans. Comput.Aided Des. Integr. Circuits Syst. 24(10): 1629\u20131637","journal-title":"IEEE Trans. Comput.Aided Des. Integr. Circuits Syst."},{"issue":"2","key":"14_CR19","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/s00165-005-0062-0","volume":"17","author":"G. Norman","year":"2005","unstructured":"Norman G., Parker D., Kwiatkowska M., Shukla S., Gupta R. (2005) Using probabilistic model checking for dynamic power management. Form. Asp. Comput. 17(2): 160\u2013176","journal-title":"Form. Asp. Comput."},{"key":"14_CR20","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-540-40981-6_9","volume-title":"Proceedings of BCS-FACS Formal Aspects of Security (FASec\u201902). LNCS","author":"G. Norman","year":"2003","unstructured":"Norman G., Shmatikov V. (2003). Analysis of probabilistic contract signing. In: Abdallah A., Ryan P., Schneider S. (eds). Proceedings of BCS-FACS Formal Aspects of Security (FASec\u201902). LNCS, vol. 2629, Springer,Berlin Heidelberg NewYork, pp. 81\u201396"},{"key":"14_CR21","unstructured":"ns-2: the Network Simulator. www.isi.edu\/nsmam\/ns"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Peterson, B., Baldwin, R., Kharoufeh, J.: A specification-compatible Bluetooth inquiry simplification. In: Procecdings of Hawaii International Conference on System Sciences (HICSS\u201904) (2004)","DOI":"10.1109\/HICSS.2004.1265720"},{"key":"14_CR23","unstructured":"PRISM Web site. www.cs.bham.ac.uk\/~dxp\/prism"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Roy, A., Gopinath, K.: Improved probabilistic models for 802.11 protocol verification. In: Procecdings of the 17th International Conference on Computer Aided Verification (CAV\u201905). LNCS, vol. 3576, pp. 239\u2013252. Springer,Berlin Heidelberg NewYork (2005)","DOI":"10.1007\/11513988_24"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Rutten J., Kwiatkowska M., Norman G., Parker D. (2004) Mathematical Techniques for analyzing concurrent and probabilistic systems, Panangaden, P., van Breugel,F. (eds.) CRM Monograph Series, vol. 23. American Mathematical Society, NewYork","DOI":"10.1090\/crmm\/023"},{"key":"14_CR26","unstructured":"Salonidis, T., Bhagwat, P., Tassiulas, L., LaMaire, R.: Proximity awareness and ad hoc network establishment in Bluetooth. Technical Report TR 2001-10. Institute of Systems Research, University of Maryland (2001)"},{"issue":"3\/4","key":"14_CR27","doi-asserted-by":"crossref","first-page":"355","DOI":"10.3233\/JCS-2004-123-403","volume":"12","author":"V. Shmatikov","year":"2004","unstructured":"Shmatikov V. (2004) Probabilistic model checking of an anonymity system. J. Comput. Secur. 12(3\/4): 355\u2013377","journal-title":"J. Comput. Secur."},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Siegemund F., Rohs M. (2002). Rendezvous layer protocols for Bluetooth-enabled smart devices. In: Proceedings of the Conference on Architecture of Computing Systems\u2014Trends in Network and Pervasive Computing (ARCS\u201902). Springer, Berlin Heidelberg NewYork","DOI":"10.1007\/3-540-45997-9_19"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Z\u00e1ruba, G., Gupta, V.: Simplified Bluetooth device discovery\u2014analysis and simulation. In: Proceedings of the Hawaii International Conference on System Sciences (HICSS\u201904) (2004)","DOI":"10.1109\/HICSS.2004.1265722"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0014-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-006-0014-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0014-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:22Z","timestamp":1559114722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-006-0014-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,5]]},"references-count":29,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,10,27]]}},"alternative-id":["14"],"URL":"https:\/\/doi.org\/10.1007\/s10009-006-0014-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,7,5]]}}}