{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:38:49Z","timestamp":1764783529540},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642404641"},{"type":"electronic","value":"9783642404658"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40465-8_2","type":"book-chapter","created":{"date-parts":[[2013,8,5]],"date-time":"2013-08-05T00:58:46Z","timestamp":1375664326000},"page":"24-47","source":"Crossref","is-referenced-by-count":12,"title":["Modeling and Analyzing Wireless Sensor Networks with VeriSensor: An Integrated Workflow"],"prefix":"10.1007","author":[{"given":"Yann","family":"Ben Maissa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabrice","family":"Kordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salma","family":"Mouline","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yann","family":"Thierry-Mieg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Adams, S., Bj\u00f6rk, M., Melham, T.F., Seger, C.-J.H.: Automatic abstraction in symbolic trajectory evaluation. In: Formal Methods in Computer-Aided Design, pp. 127\u2013135. IEEE Computer Society (2007)","DOI":"10.1109\/FAMCAD.2007.27"},{"key":"2_CR2","series-title":"LNBIP","first-page":"551","volume-title":"UNISCON","author":"B. Akbal-Delibas","year":"2009","unstructured":"Akbal-Delibas, B., Boonma, P., Suzuki, J.: Extensible and precise modeling for wireless sensor networks. In: Yang, J., Ginige, A., Mayr, H.C., Kutsche, R.-D. (eds.) UNISCON. LNBIP, vol.\u00a020, pp. 551\u2013562. Springer, Heidelberg (2009)"},{"issue":"8","key":"2_CR3","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1109\/MCOM.2002.1024422","volume":"40","author":"I.F. Akyildiz","year":"2002","unstructured":"Akyildiz, I.F., Su, W., Sankarasubramaniam, Y., Cayirci, E.: A survey on sensor networks. IEEE Communications Magazine\u00a040(8), 102\u2013114 (2002)","journal-title":"IEEE Communications Magazine"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Akyildiz, I., Vuran, M.C.: Wireless Sensor Networks. John Wiley & Sons, Inc. (2010)","DOI":"10.1002\/9780470515181"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1990","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 322\u2013335. Springer, Heidelberg (1990)"},{"key":"2_CR6","unstructured":"Baldwin, P., Kohli, S., Lee, E.A., Liu, X., Zhao, Y., Brooks, C.H., Krishnan, N.V., Neuendorffer, S., Zhong, C., Zhou, R.: Visualsense: Visual modeling for wireless and sensor network systems. Tech. rep., U.C. Berkeley (2005)"},{"key":"2_CR7","first-page":"60","volume-title":"Petri Net and Software Engineering (PNSE 2012)","author":"Y. Ben Ma\u00efssa","year":"2012","unstructured":"Ben Ma\u00efssa, Y., Kordon, F., Mouline, S., Thierry-Mieg, Y.: Modeling and Analyzing Wireless Sensor Networks with VeriSensor. In: Petri Net and Software Engineering (PNSE 2012), vol.\u00a0851, pp. 60\u201376. CEUR, Hamburg (2012)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J. Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal \u2014 a Tool Suite for Automatic Verification of Real\u2013Time Systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 232\u2013243. Springer, Heidelberg (1996)"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Boulis, A.: Castalia: revealing pitfalls in designing distributed algorithms in wsn. In: 5th International Conference on Embedded Networked Sensor Systems, pp. 407\u2013408. ACM (2007)","DOI":"10.1145\/1322263.1322318"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Boulis, A., Fehnker, A., Fruth, M., McIver, A.: Cavi\u2013simulation and model checking for wireless sensor networks. In: Fifth International Conference on Quantitative Evaluation of Systems, QEST 2008, pp. 37\u201338. IEEE (2008)","DOI":"10.1109\/QEST.2008.32"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 546\u2013550. Springer, Heidelberg (1998)"},{"key":"2_CR12","first-page":"237","volume-title":"Lecture Notes in Computer Science","author":"Marius Bozga","year":"2004","unstructured":"Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: Tools and Applications: the IF toolset. In: 4th Int. School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time, SFM-04:RT (2004)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Bucur, D., Kwiatkowska, M.Z.: Software verification for tinyos. In: 9th ACM\/IEEE International Conference on Information Processing in Sensor Networks, pp. 400\u2013401. ACM (2010)","DOI":"10.1145\/1791212.1791274"},{"key":"2_CR14","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: 5th Annual Symposium on Logic in Computer Science, pp. 1\u201333. IEEE Press (1990)"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10703-006-0033-y","volume":"31","author":"G. Ciardo","year":"2007","unstructured":"Ciardo, G., L\u00fcttgen, G., Miner, A.S.: Exploiting interleaving semantics in symbolic state-space generation. Formal Methods in System Design\u00a031(1), 63\u2013100 (2007)","journal-title":"Formal Methods in System Design"},{"key":"2_CR16","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., 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":"2_CR17","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ansi-c programs. Tools and Algorithms for the Construction and Analysis of Systems, 168\u2013176 (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"2_CR18","unstructured":"Ergen, S.C., Ergen, M., Koo, T.J.: Lifetime analysis of a sensor network with hybrid automata modelling. In: WSNA, pp. 98\u2013104 (2002)"},{"key":"2_CR19","unstructured":"Ghosh, A., Pereira, L., Yan, T.: Modeling wireless sensor network architectures using aadl. In: 4th European Congress on Embedded Real Time Software, ERTS (2008)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Gnawali, O., Welsh, M.: Sensor networks architectures and protocols. In: Emerging Wireless Technologies and the Future Mobile Internet, pp. 125\u2013153. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511921117.006"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-73368-3_45","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2007","unstructured":"Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 420\u2013432. Springer, Heidelberg (2007)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Hanna, Y., Rajan, H.: Slede: Framework for automatic verification of sensor network security protocol implementations. In: 31st International Conference on Software Engineering \u2013 Companion, pp. 427\u2013428. IEEE (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071045"},{"issue":"1-2","key":"2_CR23","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Toi, H.W.: HYTECH: A Model Checker for Hybrid Systems. Int. Journal on Software Tools for Technology Transfer\u00a01(1-2), 110\u2013122 (1997)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"2_CR24","unstructured":"Holzmann, G.: Spin model checker, the: primer and reference manual. Addison-Wesley Professional (2003)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35179-2_8","volume-title":"Transactions on Petri Nets and Other Models of Concurrency VI","author":"F. Kordon","year":"2012","unstructured":"Kordon, F., Linard, A., Buchs, D., Colange, M., Evangelista, S., Lampka, K., Lohmann, N., Paviot-Adet, E., Thierry-Mieg, Y., Wimmel, H.: Report on the Model Checking Contest at Petri Nets 2011. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) ToPNoC VI. LNCS, vol.\u00a07400, pp. 169\u2013196. Springer, Heidelberg (2012)"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Kordon, F., Linard, A., Buchs, D., Colange, M., Evangelista, S., Fronc, L., Hillah, L.M., Lohmann, N., Paviot-Adet, E., Pommereau, F., Rohr, C., Thierry-Mieg, Y., Wimmel, H., Wolf, K.: Raw Report on the Model Checking Contest at Petri Nets, Tech. rep (2012)","DOI":"10.1007\/978-3-642-35179-2_8"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Prism: Probabilistic symbolic model checker. Computer Performance Evaluation: Modelling Techniques and Tools, 113\u2013140 (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"2_CR28","unstructured":"Lee, E.A., John, I.: Overview of the ptolemy project. Electronics Research Laboratory, College of Engineering, University of California (1999)"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Levis, P., Lee, N., Welsh, M., Culler, D.: Tossim: Accurate and scalable simulation of entire tinyos applications. In: 1st International Conference on Embedded Networked Sensor Systems, pp. 126\u2013137. ACM (2003)","DOI":"10.1145\/958491.958506"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Li, P., Regehr, J.: T-check: bug finding for sensor networks. In: 9th ACM\/IEEE Int. Conf. on Information Processing in Sensor Networks, pp. 174\u2013185. ACM (2010)","DOI":"10.1145\/1791212.1791234"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Mainwaring, A., Culler, D., Polastre, J., Szewczyk, R., Anderson, J.: Wireless sensor networks for habitat monitoring. In: 1st ACM Int. Workshop on Wireless Sensor Networks and Applications (WSNA), pp. 88\u201397. ACM (2002)","DOI":"10.1145\/570738.570751"},{"key":"2_CR32","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1109\/32.825767","volume":"26","author":"N. Medvidovic","year":"2000","unstructured":"Medvidovic, N., Taylor, R.N.: A classification and comparison framework for software architecture description languages. IEEE Trans. Softw. Eng.\u00a026, 70\u201393 (2000)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Mounier, L., Samper, L., Znaidi, W.: Worst-case lifetime computation of a wireless sensor network by model-checking. In: 4th ACM Workshop on Performance Evaluation of Wireless ad Hoc, Sensor, and Ubiquitous Networks (PE-WASUN), pp. 1\u20138. ACM (2007)","DOI":"10.1145\/1298197.1298199"},{"issue":"4","key":"2_CR34","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE\u00a077(4), 541\u2013580 (1989)","journal-title":"Proceedings of the IEEE"},{"issue":"1-2","key":"2_CR35","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10990-007-9001-5","volume":"20","author":"P.C. \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation\u00a020(1-2), 161\u2013196 (2007)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-72952-5_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"P.C. \u00d6lveczky","year":"2007","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling and analysis of the OGDC wireless sensor network algorithm in real-time maude. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol.\u00a04468, pp. 122\u2013140. Springer, Heidelberg (2007)"},{"key":"2_CR37","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/j.tcs.2008.09.022","volume":"410","author":"P.C. \u00d6lveczky","year":"2009","unstructured":"\u00d6lveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in real-time maude. Theor. Comput. Sci.\u00a0410, 254\u2013280 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR38","first-page":"307","volume":"1","author":"C. Otto","year":"2005","unstructured":"Otto, C., Milenkovi\u0107, A., Sanders, C., Jovanov, E.: System architecture of a wireless body area sensor network for ubiquitous health monitoring. J. Mob. Multimed.\u00a01, 307\u2013326 (2005)","journal-title":"J. Mob. Multimed."},{"key":"2_CR39","unstructured":"Sadilek, D.A.: Domain-specific languages for wireless sensor networks. In: Modellierung, pp. 237\u2013241 (2008)"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)"},{"key":"2_CR41","unstructured":"Thierry-Mieg, Y., B\u00e9rard, B., Kordon, F., Lime, D., Roux, O.H.: Compositional Analysis of Discrete Time Petri nets. In: 1st Workshop on Petri Nets Compositions (CompoNet 2011), vol.\u00a0726, pp. 17\u201331. CEUR (2011)"},{"key":"2_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-44919-1_9","volume-title":"Applications and Theory of Petri Nets 2003","author":"Y. Thierry-Mieg","year":"2003","unstructured":"Thierry-Mieg, Y., Dutheillet, C., Mounier, I.: Automatic symmetry detection in well-formed nets. In: van der Aalst, W.M.P., Best, E. (eds.) ICATPN 2003. LNCS, vol.\u00a02679, pp. 82\u2013101. Springer, Heidelberg (2003)"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00768-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Thierry-Mieg","year":"2009","unstructured":"Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical Set Decision Diagrams and Regular Models. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 1\u201315. Springer, Heidelberg (2009)"},{"issue":"3","key":"2_CR44","first-page":"293","volume":"4","author":"Y. Thierry-Mieg","year":"2008","unstructured":"Thierry-Mieg, Y., Hillah, L.-M.: UML behavioral consistency checking using Instantiable Petri nets. ISSE\u00a04(3), 293\u2013300 (2008)","journal-title":"ISSE"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"Tschirner, S., Xuedong, L., Yi, W.: Model-based validation of QoS properties of biomedical sensor networks. In: 8th Int. Conf. on Embedded Software, pp. 69\u201378. ACM (2008)","DOI":"10.1145\/1450058.1450069"},{"issue":"3\/4","key":"2_CR46","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1142\/S021884300700172X","volume":"16","author":"C. Vicente-Chicote","year":"2007","unstructured":"Vicente-Chicote, C., Losilla, F., \u00c1lvarez, B., Iborra, A., S\u00e1nchez, P.: Applying mde to the development of flexible and reusable wireless sensor networks. Int. J. Cooperative Inf. Syst.\u00a016(3\/4), 393\u2013412 (2007)","journal-title":"Int. J. Cooperative Inf. Syst."},{"key":"2_CR47","unstructured":"Wada, H., Boonma, P., Suzuki, J., Oba, K.: Modeling and executing adaptive sensor network applications with the Matilda UML virtual machine. In: 11th IASTED Int. Conf. on Software Engineering and Applications (SEA), pp. 216\u2013225. ACTA Press (2007)"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"Watteyne, T., Aug\u00e9-Blum, I., Ub\u00e9da, S.: Dual-mode real-time mac protocol for wireless sensor networks: a validation\/simulation approach. In: 1st Int. Conf. on Integrated Internet ad hoc and Sensor Networks (InterSense), ACM (2006)","DOI":"10.1145\/1142680.1142683"},{"issue":"2","key":"2_CR49","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":"2_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-24559-6_26","volume-title":"Formal Methods and Software Engineering","author":"M. Zheng","year":"2011","unstructured":"Zheng, M., Sun, J., Liu, Y., Dong, J.S., Gu, Y.: Towards a model checker for NesC and wireless sensor networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 372\u2013387. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency VIII"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40465-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,20]],"date-time":"2019-07-20T10:23:11Z","timestamp":1563618191000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40465-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642404641","9783642404658"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40465-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}