{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:22:08Z","timestamp":1742916128145,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030670863"},{"type":"electronic","value":"9783030670870"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-67087-0_7","type":"book-chapter","created":{"date-parts":[[2021,1,14]],"date-time":"2021-01-14T01:17:39Z","timestamp":1610587059000},"page":"94-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Exploring IoT Trickle-Based Dissemination Using Timed Model-Checking and Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Boutheina","family":"Bannour","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnault","family":"Lapitre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascale","family":"Le Gall","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,14]]},"reference":[{"key":"7_CR1","unstructured":"RPL: IPv6 routing protocol for low-power and lossy networks, request for comments: 6550. Technical report, Cooper Power Systems and Cisco Systems and Stanford University, March 2012 (2012)"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. J. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"J. Theoret. Comput. Sci."},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2016.01.003","volume":"320","author":"M Arnaud","year":"2016","unstructured":"Arnaud, M., Bannour, B., Lapitre, A.: An illustrative use case of the DIVERSITY platform based on UML interaction scenarios. Electr. Notes Theoret. Comput. Sci. 320, 21\u201334 (2016)","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-34691-0_10","volume-title":"Testing Software and Systems","author":"B Bannour","year":"2012","unstructured":"Bannour, B., Escobedo, J.P., Gaston, C., Le Gall, P.: Off-line test case generation for timed symbolic model-based conformance testing. In: Nielsen, B., Weise, C. (eds.) ICTSS 2012. LNCS, vol. 7641, pp. 119\u2013135. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34691-0_10"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Bannour, B., Lapitre, A.: Heuristic-aided symbolic simulation for trickle-based wireless sensors networks configuration. In: International Workshop on RAPIDO@HiPEAC. ACM (2020)","DOI":"10.1145\/3375246.3375255"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"7_CR7","series-title":"Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-30422-4_10","volume-title":"Mobile Networks and Management","author":"M Becker","year":"2012","unstructured":"Becker, M., Kuladinithi, K., G\u00f6rg, C.: Modelling and simulating the Trickle algorithm. In: Pentikousis, K., Aguiar, R., Sargento, S., Ag\u00fcero, R. (eds.) MONAMI 2011. LNICST, vol. 97, pp. 135\u2013144. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30422-4_10"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Breza, M.J., McCann, J.A.: Lessons in implementing bio-inspired algorithms on wireless sensor networks. In: International Conference on NASA\/ESA. IEEE (2008)","DOI":"10.1109\/AHS.2008.72"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Chen, Z., Zhang, D., Zhu, R., Ma, Y., Yin, P., Xie, F.: A review of automated formal verification of ad hoc routing protocols for wireless sensor networks. CoRR, abs\/1305.7410 (2013)","DOI":"10.1166\/sl.2013.2653"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-69850-0_12","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 196\u2013215. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_12"},{"key":"7_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Coladon, T., Vucinic, M., Tourancheau, B.: Multiple redundancy constants with trickle. In: PIMRC. IEEE (2015)","DOI":"10.1109\/PIMRC.2015.7343618"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197\u2013212. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_17"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-88194-0_20","volume-title":"Formal Methods and Software Engineering","author":"JS Dong","year":"2008","unstructured":"Dong, J.S., Sun, J., Sun, J., Taguchi, K., Zhang, X.: Specifying and verifying sensor networks: an experiment of formal methods. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 318\u2013337. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88194-0_20"},{"key":"7_CR16","unstructured":"Dunkels, A., Gronvall, B., Voigt, T.: Contiki - a lightweight and flexible operating system for tiny networked sensors. In: IEEE ICLCN (2004)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Hui, J., Kelsey, R.: Multicast protocol for low-power and lossy networks, request for comments: 7731. Technical report, Silicon Labs (2016)","DOI":"10.17487\/RFC7731"},{"key":"7_CR18","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19, 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"7_CR19","doi-asserted-by":"publisher","first-page":"1960","DOI":"10.1109\/LCOMM.2012.111612.121232","volume":"16","author":"HR Kermajani","year":"2012","unstructured":"Kermajani, H.R., Gomez, C., Arshad, M.H.: Modeling the message count of the Trickle algorithm in a steady-state, static wireless sensor network. IEEE Commun. Lett. 16, 1960\u20131963 (2012)","journal-title":"IEEE Commun. Lett."},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1481506.1481511","volume":"36","author":"MZ Kwiatkowska","year":"2008","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Analysis of a gossip protocol in PRISM. SIGMETRICS Perform. Eval. Rev. 36, 17\u201322 (2008)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Lee, B., Song, H.K., Suh, Y., Oh, K.H., Youn, H.Y.: Energy-efficient gossiping protocol of WSN with realtime streaming data. In: International Conference on DASC (2014)","DOI":"10.1109\/DASC.2014.47"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Levis, P., Clausen, T., Hui, J., Gnawali, O., Ko, J.: The Trickle algorithm, request for comments: 6206. Technical report, March 2011 (2011)","DOI":"10.17487\/rfc6206"},{"key":"7_CR24","volume-title":"Ambient Intelligence","author":"P Levis","year":"2005","unstructured":"Levis, P., et al.: TinyOS: an operating system for sensor networks. In: Weber, W., Rabaey, J.M., Aarts, E. (eds.) Ambient Intelligence. Springer, Heidelberg (2005)"},{"key":"7_CR25","unstructured":"Levis, P., Patel, N., Culler, D., Shenker, S.: Trickle: a self-regulating algorithm for code propagation and maintenance in wireless sensor networks. In: International Symposium on NSDI. USENIX Association (2004)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: PAT 3: an extensible architecture for building multi-domain model checkers. In: Dohi, T., Cukic, B. (eds.) International Conference on ISSRE. IEEE (2011)","DOI":"10.1109\/ISSRE.2011.19"},{"key":"7_CR27","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s11134-015-9438-x","volume":"81","author":"T Meyfroyt","year":"2015","unstructured":"Meyfroyt, T., Borst, S.C., Boxma, O.J., Denteneer, D.: On the scalability and message count of Trickle-based broadcasting schemes. Queueing Syst. 81, 203\u2013230 (2015)","journal-title":"Queueing Syst."},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Meyfroyt, T.M.M.: An analytic evaluation of the Trickle algorithm: towards efficient, fair, fast and reliable data dissemination. In: WoWMoM. IEEE (2015)","DOI":"10.1109\/WoWMoM.2015.7158155"},{"key":"7_CR29","first-page":"1","volume":"2018","author":"X Nan","year":"2018","unstructured":"Nan, X., Fei, M., Yang, T.: Randomized and efficient time synchronization in dynamic wireless sensor networks: a gossip-consensus-based approach. Complexity 2018, 1\u201316 (2018)","journal-title":"Complexity"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Nguyen, N.M.T., Bannour, B., Lapitre, A., Le Gall, P.: Behavioral models and scenario selection for testing IoT Trickle-based lossy multicast networks. In: International Workshop on VVIoT@ICST. IEEE (2019)","DOI":"10.1109\/ICSTW.2019.00047"},{"key":"7_CR31","first-page":"1477","volume":"4","author":"M Vucinic","year":"2017","unstructured":"Vucinic, M., Kr\u00f3l, M., Jonglez, B., Coladon, T., Tourancheau, B.: Trickle-D: high fairness and low transmission load with dynamic redundancy. IEEE IoT J. 4, 1477\u20131488 (2017)","journal-title":"IEEE IoT J."},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Webster, M., Breza, M., Dixon, C., Fisher, M., McCann, J.A.: Formal verification of synchronisation, gossip and environmental effects for wireless sensor networks. In: ECEASST (2018)","DOI":"10.29007\/qb84"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-30729-4_12","volume-title":"Integrated Formal Methods","author":"M Woehrle","year":"2012","unstructured":"Woehrle, M., Bakhshi, R., Mousavi, M.R.: Mechanized extraction of topology anti-patterns in wireless networks. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 158\u2013173. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_12"},{"key":"7_CR34","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, Yu.: Towards a model checker for NesC and wireless sensor networks. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 372\u2013387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24559-6_26"}],"container-title":["Lecture Notes in Computer Science","Networked Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67087-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,14]],"date-time":"2021-01-14T01:45:49Z","timestamp":1610588749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-67087-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030670863","9783030670870"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-67087-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"14 January 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NETYS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Networked Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakech","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 June 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 June 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"netys2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/netys.net\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"39% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.75","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually. Three invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}