{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:49Z","timestamp":1725533929290},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026515"},{"type":"electronic","value":"9783642026522"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02652-2_19","type":"book-chapter","created":{"date-parts":[[2009,6,25]],"date-time":"2009-06-25T11:43:06Z","timestamp":1245930186000},"page":"223-240","source":"Crossref","is-referenced-by-count":12,"title":["Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin"],"prefix":"10.1007","author":[{"given":"Oliver","family":"Sharma","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Lewis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alice","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Al","family":"Dearle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dharini","family":"Balasubramaniam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ron","family":"Morrison","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joe","family":"Sventek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"19_CR1","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/S1389-1286(01)00302-4","volume":"38","author":"I. Akyildiz","year":"2002","unstructured":"Akyildiz, I., Su, W., Sankarasubramaniam, Y., Cyirici, E.: Wireless sensor networks: A survey. Computer Networks\u00a038(4), 393\u2013422 (2002)","journal-title":"Computer Networks"},{"key":"19_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters\u00a022, 307\u2013309 (1986)","journal-title":"Information Processing Letters"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-78789-1_16","volume-title":"Software Composition","author":"D. Balasubramaniam","year":"2008","unstructured":"Balasubramaniam, D., Dearle, A., Morrison, R.: A composition-based approach to the construction and dynamic reconfiguration of wireless sensor network applications. In: Pautasso, C., Tanter, \u00c9. (eds.) SC 2008. LNCS, vol.\u00a04954, pp. 206\u2013214. Springer, Heidelberg (2008)"},{"key":"19_CR4","first-page":"255","volume-title":"Proc. of the 2nd Int\u2019l. Symp. on leveraging applications of formal methods","author":"P. Ballarini","year":"2006","unstructured":"Ballarini, P., Miller, A.: Model checking medium access control for sensor networks. In: Proc. of the 2nd Int\u2019l. Symp. on leveraging applications of formal methods, pp. 255\u2013262. IEEE, Los Alamitos (2006)"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s100090200074","volume":"4","author":"D. Bosnacki","year":"2002","unstructured":"Bosnacki, D., Dams, D., Holenderski, L.: Symmetric Spin. International Journal on Software Tools for Technology Transfer\u00a04(1), 65\u201380 (2002)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"11-12","key":"19_CR6","doi-asserted-by":"publisher","first-page":"1257","DOI":"10.1002\/spe.767","volume":"36","author":"\u00c9. Bruneton","year":"2006","unstructured":"Bruneton, \u00c9., Coupaye, T., Leclercq, M., Qu\u00e9ma, V., Stefani, J.-B.: The fractal component model and its support in Java. Software Practice and Experience\u00a036(11-12), 1257\u20131284 (2006)","journal-title":"Software Practice and Experience"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of the 1st Workshop in Logic of Programs","author":"E. Clarke","year":"1981","unstructured":"Clarke, E., Emerson, E.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131. Springer, Heidelberg (1981)"},{"issue":"2","key":"19_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"19_CR9","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"19_CR10","first-page":"1303","volume-title":"Proc. of the 32nd Int\u2019l Computer Software and Applications Conference (COMPSAC 2008)","author":"A. Dearle","year":"2008","unstructured":"Dearle, A., Balasubramaniam, D., Lewis, J., Morrison, R.: A component-based model and language for wireless sensor network applications. In: Proc. of the 32nd Int\u2019l Computer Software and Applications Conference (COMPSAC 2008), pp. 1303\u20131308. IEEE Computer Society Press, Los Alamitos (2008)"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/11784180_29","volume-title":"Algebraic Methodology and Software Technology","author":"A.F. Donaldson","year":"2006","unstructured":"Donaldson, A.F., Miller, A.: A computational group theoretic symmetry reduction package for the SPIN model checker. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 374\u2013380. Springer, Heidelberg (2006)"},{"key":"19_CR12","volume-title":"Proc. 1st Workshop on Embedded Networked Sensors (EmNets-I)","author":"A. Dunkels","year":"2004","unstructured":"Dunkels, A., Gr\u00f6nvall, B., Voigt, T.: Contiki \u2013 a lightweight and flexible operating system for tiny networked sensors. In: Proc. 1st Workshop on Embedded Networked Sensors (EmNets-I). IEEE, Los Alamitos (2004)"},{"issue":"4","key":"19_CR13","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/1274858.1274860","volume":"6","author":"D. Gay","year":"2007","unstructured":"Gay, D., Levis, P., Culler, D.: Software design patterns for TinyOS. Transactions on Embedded Computing Systems\u00a06(4), 22 (2007)","journal-title":"Transactions on Embedded Computing Systems"},{"key":"19_CR14","volume-title":"The SPIN model checker: primer and reference manual","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN model checker: primer and reference manual. Addison Wesley, Boston (2003)"},{"key":"19_CR15","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/COMSWA.2008.4554369","volume-title":"Proc. 3rd Int\u2019l. Conference on Communication Systems Software and Middleware (COMSWARE 2008)","author":"A. Khan","year":"2008","unstructured":"Khan, A., Jenkins, L.: Undersea wireless sensor network for ocean pollution prevention. In: Proc. 3rd Int\u2019l. Conference on Communication Systems Software and Middleware (COMSWARE 2008), pp. 2\u20138. IEEE, Los Alamitos (2008)"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1145\/72981.72998","volume-title":"Proceedings of the eighth Annual ACM Symposium on Principles of Distrubuted Computing","author":"R.P. Kurshan","year":"1989","unstructured":"Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. In: Proceedings of the eighth Annual ACM Symposium on Principles of Distrubuted Computing, pp. 239\u2013247. ACM Press, New York (1989)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-45605-8_11","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Kwiatkowska","year":"2002","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.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 169\u2013187. Springer, Heidelberg (2002)"},{"issue":"2","key":"19_CR18","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1016\/j.comnet.2006.08.009","volume":"51","author":"A. Miller","year":"2007","unstructured":"Miller, A., Calder, M., Donaldson, A.F.: A template-based approach for the generation of abstractable and reducible models of featured networks. Computer Networks\u00a051(2), 439\u2013455 (2007)","journal-title":"Computer Networks"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. Computing Surveys\u00a036(3) (2006)","DOI":"10.1145\/1132960.1132962"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Skordylis, A., Guitton, A., Trigoni, N.: Correlation-based data dissemination in traffic monitoring sensor networks. In: Proc. 2nd int\u2019l. conference on emerging networking experiments and Technoligies (CoNext 2006), p. 42 (2006)","DOI":"10.1145\/1368436.1368487"},{"key":"19_CR21","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-0-387-74899-3_9","volume-title":"Wireless Sensor and Actor Networks","author":"L. Tobarra","year":"2007","unstructured":"Tobarra, L., Cazorla, D., Cuatero, F., Diaz, G., Cambronero, E.: Model checking wirelss sensor network security protocols: TinySec + LEAP. In: Wireless Sensor and Actor Networks. IFIP International Federation for Information Processing, vol.\u00a0248, pp. 95\u2013106. Springer, Heidelberg (2007)"},{"key":"19_CR22","first-page":"378","volume-title":"Proc. 29th Int\u2019l. Conference on Engineering in Medicine and Biology (EMBS\u201907)","author":"S. Venkatraman","year":"2007","unstructured":"Venkatraman, S., Long, J., Pister, K., Carmena, J.: Wireless inertial sensors for monitoring animal behaviour. In: Proc. 29th Int\u2019l. Conference on Engineering in Medicine and Biology (EMBS 2007), pp. 378\u2013381. IEEE, Los Alamitos (2007)"},{"issue":"2","key":"19_CR23","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MIC.2006.26","volume":"10","author":"G. Werner-Allen","year":"2006","unstructured":"Werner-Allen, G., Lorincz, K., Welsh, M., Marcillo, O., Johnson, J., Ruiz, M., Lees, J.: Deploying a wireless sensor network on an active volcano. IEEE Internet Computing\u00a010(2), 18\u201325 (2006)","journal-title":"IEEE Internet Computing"},{"key":"19_CR24","unstructured":"Xie, F., Song, X., Chung, H., Nandi, R.: Translation-based co-verification. In: Proceedings of the 3rd International Conference on Formal Methods and Models for Codesign, Verona, Italy, pp. 111\u2013120. ACM-IEEE, IEEE Computer Society (2005)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02652-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T23:32:57Z","timestamp":1552087977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02652-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026515","9783642026522"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02652-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}