{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:12:09Z","timestamp":1725520329985},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540881933"},{"type":"electronic","value":"9783540881940"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-88194-0_20","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T10:56:21Z","timestamp":1224240981000},"page":"318-337","source":"Crossref","is-referenced-by-count":13,"title":["Specifying and Verifying Sensor Networks: An Experiment of Formal Methods"],"prefix":"10.1007","author":[{"given":"Jin Song","family":"Dong","sequence":"first","affiliation":[]},{"given":"Jing","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Kenji","family":"Taguchi","sequence":"additional","affiliation":[]},{"given":"Xian","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"20_CR1","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/S1389-1286(01)00302-4","volume":"38","author":"I.F. Akyildiz","year":"2002","unstructured":"Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: Wireless Sensor Networks: a Survey. Computer Networks\u00a038(4), 393\u2013422 (2002)","journal-title":"Computer Networks"},{"issue":"6","key":"20_CR2","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1023\/A:1012319418150","volume":"7","author":"P. Bose","year":"2001","unstructured":"Bose, P., Morin, P., Stojmenovic, I., Urrutia, J.: Routing with Guaranteed Delivery in Ad Hoc Wireless Networks. Wireless Networks\u00a07(6), 609\u2013616 (2001)","journal-title":"Wireless Networks"},{"key":"20_CR3","unstructured":"Botts, M.: Sensor Model Language (SensorML) (2006), http:\/\/vast.nsstc.uah.edu\/SensorML\/"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Boulis, A., Han, C.C., Srivastava, M.B.: Design and Implementation of a Framework for Efficient and Programmable Sensor Networks. In: Proceedings of International Conference on Mobile Systems, Applictions, and Services (MobiSys 2003) (2003)","DOI":"10.1145\/1066116.1066121"},{"issue":"1","key":"20_CR5","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(99)00231-5","volume":"240","author":"L. Cardelli","year":"2000","unstructured":"Cardelli, L., Gordon, A.D.: Mobile Ambients. Theoretical Computer Science\u00a0240(1), 177\u2013213 (2000)","journal-title":"Theoretical Computer Science"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053547","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Cardelli","year":"1998","unstructured":"Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol.\u00a01378. Springer, Heidelberg (1998)"},{"key":"20_CR7","first-page":"271","volume-title":"Proceedings of the 30th International Conference on Software Engineering (ICSE 2008)","author":"C. Chen","year":"2008","unstructured":"Chen, C., Dong, J.S., Sun, J.: A verification system for timed interval calculus. In: Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), pp. 271\u2013280. ACM Press, New York (2008)"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Ciancio, A.G., Pattem, S., Ortega, A., Krishnamachari, B.: Energy-efficient Data Representation and Routing for Wireless Sensor Networks based on a Distributed Wavelet Compression Algorithm. In: Proceedings of Information Processing in Sensor Networks (IPSN 2006), pp. 309\u2013316 (2006)","DOI":"10.1145\/1127777.1127824"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-540-30482-1_39","volume-title":"Formal Methods and Software Engineering","author":"J.S. Dong","year":"2004","unstructured":"Dong, J.S., Hao, P., Qin, S.C., Sun, J., Wang, Y.: Timed Patterns: TCOZ to Timed Automata. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 483\u2013498. Springer, Heidelberg (2004)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11901433_19","volume-title":"Formal Methods and Software Engineering","author":"J.S. Dong","year":"2006","unstructured":"Dong, J.S., Hao, P., Sun, J., Zhang, X.: A Reasoning Method for Timed CSP Based on Constraint Solving. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 342\u2013359. Springer, Heidelberg (2006)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Estrin, D., Govindan, R., Heidemann, J., Kumar, S.: Next Century Challenges: Scalable Coordination in Sensor Networks. In: Proceedings of ACM\/IEEE International Conference on Mobile Computing and Networking (MobiCom 1999), pp. 263\u2013270 (1999)","DOI":"10.1145\/313451.313556"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Frey, H., Stojmenovic, I.: On Delivery Guarantees of Face and Combined Greedy-face Routing in Ad Hoc and Sensor Networks. In: Proceedings of the 12th Annual International Conference on Mobile Computing and Networking (MOBICOM 2006), pp. 390\u2013401 (2006)","DOI":"10.1145\/1161089.1161133"},{"key":"20_CR14","first-page":"1","volume-title":"Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003 (PLDI 2003)","author":"D. Gay","year":"2003","unstructured":"Gay, D., Levis, P., von Behren, J.R., Welsh, M., Brewer, E.A., Culler, D.E.: The nesC Language: A Holistic Approach to Networked Embedded Systems. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003 (PLDI 2003), pp. 1\u201311. ACM Press, New York (2003)"},{"key":"20_CR15","first-page":"302","volume-title":"Proceedings of the 28th International Conference on Software Engineering (ICSE 2006)","author":"A. Goel","year":"2006","unstructured":"Goel, A., Meng, S., Roychoudhury, A., Thiagarajan, P.S.: Interacting process classes. In: Proceedings of the 28th International Conference on Software Engineering (ICSE 2006), pp. 302\u2013311. ACM Press, New York (2006)"},{"key":"20_CR16","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Intanagonwiwat, C., Govindan, R., Estrin, D.: Directed Diffusion: a Scalable and Robust Communication Paradigm for Sensor Networks. In: Proceedings of International Conference on Mobile Computing and Networking (MOBICOM 2000), pp. 56\u201367 (2000)","DOI":"10.1145\/345910.345920"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11560548_14","volume-title":"Correct Hardware Design and Verification Methods","author":"L. Lamport","year":"2005","unstructured":"Lamport, L.: Real-Time Model Checking Is Really Simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 162\u2013175. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"20_CR19","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Wang, Y.: Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Levis, P., Culler, D.E.: Mat\u00e9: a Tiny Virtual Machine for Sensor Networks. In: Proceedings of International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2002), pp. 85\u201395 (2002)","DOI":"10.1145\/605397.605407"},{"key":"20_CR21","unstructured":"Levis, P., Patel, N., Culler, D.E., Shenker, S.: Trickle: A Self-Regulating Algorithm for Code Propagation and Maintenance in Wireless Sensor Networks. In: Proceedings of Networked Systems Design and Implementation (NSDI 2004), pp. 15\u201328 (2004)"},{"issue":"1","key":"20_CR22","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1145\/1061318.1061322","volume":"30","author":"S. Madden","year":"2005","unstructured":"Madden, S., Franklin, M.J., Hellerstein, J.M., Hong, W.: TinyDB: an Acquisitional Query Processing System for Sensor Networks. ACM Transactions on Database Systems\u00a030(1), 122\u2013173 (2005)","journal-title":"ACM Transactions on Database Systems"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Mahony, B., Dong, J.S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering\u00a026(2) (February 2000)","DOI":"10.1109\/32.841115"},{"key":"20_CR24","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/j.entcs.2006.04.017","volume":"158","author":"N. Mezzetti","year":"2006","unstructured":"Mezzetti, N., Sangiorgi, D.: Towards a Calculus For Wireless Systems. Electronic Notes in Theoretical Computer Science\u00a0158, 331\u2013353 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-53982-4_19","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"K.V.S. Prasad","year":"1991","unstructured":"Prasad, K.V.S.: A Calculus of Broadcasting Systems. In: Abramsky, S. (ed.) TAPSOFT 1991. LNCS, vol.\u00a0493, pp. 338\u2013358. Springer, Heidelberg (1991)"},{"issue":"2","key":"20_CR26","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1995.1014","volume":"116","author":"S. Schneider","year":"1995","unstructured":"Schneider, S.: An Operational Semantics for Timed CSP. Information and Computation\u00a0116(2), 193\u2013213 (1995)","journal-title":"Information and Computation"},{"key":"20_CR27","first-page":"640","volume":"600","author":"S. Schneider","year":"1992","unstructured":"Schneider, S., Davies, J., Jackson, D.M., Reed, G.M., Reed, J.N., Roscoe, A.W.: Timed CSP: Theory and practice. Real-Time: Theory in Practice\u00a0600, 640\u2013675 (1992)","journal-title":"Real-Time: Theory in Practice"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Sun, J., Dong, J.S.: Design Synthesis from Interaction and State-Based Specifications. IEEE Transactions on Software Engineering\u00a032(6) (2006)","DOI":"10.1109\/TSE.2006.55"},{"key":"20_CR29","first-page":"23","volume-title":"Proceedings of the Second IEEE International Symposium on Theoretical Aspects of Software Engineering","author":"J. Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S., Sun, J.: Bounded Model Checking of Compositional Processes. In: Proceedings of the Second IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 23\u201330. IEEE Computer Society Press, Los Alamitos (2008)"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Thomsen, B.: Calculi for Higher Order Communicating Systems. PhD thesis (1990)","DOI":"10.1145\/75277.75290"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Tschirner, S., Xuedong, L., Yi, W.: Model-Based Validation of QoS Properties of Biomedical Sensor Networks. In: Proceedings of the International Conference on Embedded Software (EMSOFT 2008) (accepted, 2008)","DOI":"10.1145\/1450058.1450069"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"von Eicken, T., Culler, D.E., Goldstein, S.C., Schauser, K.E.: Active Messages: A Mechanism for Integrated Communication and Computation. In: Proceedings of International Symposium on Computer Architecture 1992 (ISCA 1992), pp. 256\u2013266 (1992)","DOI":"10.1145\/139669.140382"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T15:08:10Z","timestamp":1557846490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}