{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:27:32Z","timestamp":1750307252086,"version":"3.41.0"},"reference-count":122,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2011,1]]},"abstract":"<jats:p>Wireless self-organizing networks (WSONs) have attracted considerable attention from the network research community; however, the key for their success is the rigorous validation of the properties of the network protocols. Applications of risk or those demanding precision (like alert-based systems) require a rigorous and reliable validation of deployed network protocols. While the main goal is to ensure the reliability of the protocols, validation techniques also allow the establishment of their correctness regarding the related protocols' requirements. Nevertheless, even if different communities have carried out intensive research activities on the validation domain, WSONs still raise new issues for and challenging constraints to these communities. We thus, advocate the use of complementary techniques coming from different research communities to efficiently address the validation of WSON protocols. The goal of this tutorial is to present a comprehensive review of the literature on protocol engineering techniques and to discuss difficulties imposed by the characteristics of WSONs on the protocol engineering community. Following the formal and nonformal classification of techniques, we provide a discussion about components and similarities of existing protocol validation approaches. We also investigate how to take advantage of such similarities to obtain complementary techniques and outline new challenges.<\/jats:p>","DOI":"10.1145\/1883612.1883614","type":"journal-article","created":{"date-parts":[[2011,2,1]],"date-time":"2011-02-01T15:50:21Z","timestamp":1296575421000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["One step forward"],"prefix":"10.1145","volume":"43","author":[{"given":"Aline Carneiro","family":"Viana","sequence":"first","affiliation":[{"name":"INRIA, Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephane","family":"Maag","sequence":"additional","affiliation":[{"name":"TELECOM &amp; Management SudParis and Samovar CNRS, Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fatiha","family":"Zaidi","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Sud, LRI UMR 8623, Orsay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,2,4]]},"reference":[{"volume-title":"Methods for testing and specification (MTS)","key":"e_1_2_1_1_1","unstructured":"ETSI. 2007. Methods for testing and specification (MTS) ; The testing and test control notation version 3; part 1: Ttcn-3 core language, v3.2.1. Tech. rep., 873-1, ETSI, Sophia Antipolis, France . ETSI. 2007. Methods for testing and specification (MTS); The testing and test control notation version 3; part 1: Ttcn-3 core language, v3.2.1. Tech. rep., 873-1, ETSI, Sophia Antipolis, France."},{"volume-title":"Information technology\u2014open systems interconnection\u2014conformance testing methodology and framework--part 1: General concepts. Tech. rep., 9646-1","key":"e_1_2_1_2_1","unstructured":"ISO. 1994. Information technology\u2014open systems interconnection\u2014conformance testing methodology and framework--part 1: General concepts. Tech. rep., 9646-1 , ISO , Genewa, Switzerland . ISO. 1994. Information technology\u2014open systems interconnection\u2014conformance testing methodology and framework--part 1: General concepts. Tech. rep., 9646-1, ISO, Genewa, Switzerland."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76809-8_4"},{"key":"e_1_2_1_4_1","first-page":"321","article-title":"Automata for modeling real-time systems","volume":"443","author":"Alur R.","year":"1990","unstructured":"Alur , R. and Dill , D. 1990 . Automata for modeling real-time systems . In Proceedings of the International Colloquium on Automata, Languages and Programming. Vol. 443. 321 -- 335 . Alur, R. and Dill, D. 1990. Automata for modeling real-time systems. In Proceedings of the International Colloquium on Automata, Languages and Programming. Vol. 443. 321--335.","journal-title":"Proceedings of the International Colloquium on Automata, Languages and Programming."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.242"},{"volume-title":"Proceedings of the DARPA\/NIST Network Simulation Validation Workshop.","author":"Bagrodia R.","key":"e_1_2_1_6_1","unstructured":"Bagrodia , R. and Takai , M . 1999. Position paper on validation of network simulation models . In Proceedings of the DARPA\/NIST Network Simulation Validation Workshop. Bagrodia, R. and Takai, M. 1999. Position paper on validation of network simulation models. In Proceedings of the DARPA\/NIST Network Simulation Validation Workshop."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/268437.268462"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.16"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2004.09.009"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11422778_93"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.988495"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/49.840210"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.59"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Bolch G. Greiner S. de Meer H. and Trivedi K. S. 2006. Queueing Networks and Markov Chains. John Wiley and Sons New York NY.   Bolch G. Greiner S. de Meer H. and Trivedi K. S. 2006. Queueing Networks and Markov Chains. John Wiley and Sons New York NY.","DOI":"10.1002\/0471791571"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1987.1096769"},{"key":"e_1_2_1_17_1","first-page":"212","article-title":"Formal verification of a multicast protocol in mobile networks","volume":"1","author":"Borujerdi M. M.","year":"2004","unstructured":"Borujerdi , M. M. and Mirzababaei , S. M. 2004 . Formal verification of a multicast protocol in mobile networks . Int. J. Signal Proc. 1 , 4, 212 -- 218 . Borujerdi, M. M. and Mirzababaei, S. M. 2004. Formal verification of a multicast protocol in mobile networks. Int. J. Signal Proc. 1, 4, 212--218.","journal-title":"Int. J. Signal Proc."},{"volume-title":"Proceedings of the 16th International Conference on Formal Description Techniques: Theory, application and tools. Chapman &amp; Hall, Ltd.","author":"B\u00fctow M.","key":"e_1_2_1_18_1","unstructured":"B\u00fctow , M. , Mestern , M. , Schapiro , C. , and Kritzinger , P. S . 1996. Performance modelling with the formal specification language sdl . In Proceedings of the 16th International Conference on Formal Description Techniques: Theory, application and tools. Chapman &amp; Hall, Ltd. , London, U.K., 213--228. B\u00fctow, M., Mestern, M., Schapiro, C., and Kritzinger, P. S. 1996. Performance modelling with the formal specification language sdl. In Proceedings of the 16th International Conference on Formal Description Techniques: Theory, application and tools. Chapman &amp; Hall, Ltd., London, U.K., 213--228."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24704-3_2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/584490.584499"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_7"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1023756.1023758"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11494881_20"},{"volume-title":"Proceedings of 1st Workshop on ITU System Design Languages.","author":"Christmann D.","key":"e_1_2_1_24_1","unstructured":"Christmann , D. , Becker , P. , Gotzhein , R. , and Kuhn , T . 2008. Model-driven development of a MAC layer for ad-hoc networks with SDL . In Proceedings of 1st Workshop on ITU System Design Languages. Christmann, D., Becker, P., Gotzhein, R., and Kuhn, T. 2008. Model-driven development of a MAC layer for ad-hoc networks with SDL. In Proceedings of 1st Workshop on ITU System Design Languages."},{"volume-title":"Proceedings of the 1st Workshop on Logic of Programs.","author":"Clarke E. M.","key":"e_1_2_1_25_1","unstructured":"Clarke , E. M. and Emerson , E. A . 1981. Synthesis of synchronization skeletons for branching time temporal logic . In Proceedings of the 1st Workshop on Logic of Programs. Clarke, E. M. and Emerson, E. A. 1981. Synthesis of synchronization skeletons for branching time temporal logic. In Proceedings of the 1st Workshop on Logic of Programs."},{"key":"e_1_2_1_26_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA.   Clarke E. M. Grumberg O. and Peled D. A. 1999. Model Checking. MIT Press Cambridge MA."},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Clausen T. and Jacquet P. 2003. RFC3626: Optimized link state routing protocol (OLSR). www.ietf.org.   Clausen T. and Jacquet P. 2003. RFC3626: Optimized link state routing protocol (OLSR). www.ietf.org.","DOI":"10.17487\/rfc3626"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"volume-title":"A survey of simulation in sensor networks. Tech. rep","author":"Curren D.","key":"e_1_2_1_29_1","unstructured":"Curren , D. 2005. A survey of simulation in sensor networks. Tech. rep . University of Binghamton , Binghamton, NY . www.cs.binghamton.edu\/~kang\/teaching\/cs580s\/david.pdf. Curren, D. 2005. A survey of simulation in sensor networks. Tech. rep. University of Binghamton, Binghamton, NY. www.cs.binghamton.edu\/~kang\/teaching\/cs580s\/david.pdf."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1035334.1035338"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science","volume":"2517","author":"Das S.","unstructured":"Das , S. and Dill , D. L . 2002. Counter-example based predicate discovery in predicate abstraction . In Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science , vol. 2517 . Springer-Verlag, Berlin, Germany, 19--32. Das, S. and Dill, D. L. 2002. Counter-example based predicate discovery in predicate abstraction. In Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 2517. Springer-Verlag, Berlin, Germany, 19--32."},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"de Alfaro L. Faella M. and Stoelinga M. I. A. 2004. Linear and branching metrics for quantitative transition systems. Lecture Notes in Computer Science vol. 3142. Springer-Verlag Berlin Germany 97--109.  de Alfaro L. Faella M. and Stoelinga M. I. A. 2004. Linear and branching metrics for quantitative transition systems. Lecture Notes in Computer Science vol. 3142. Springer-Verlag Berlin Germany 97--109.","DOI":"10.1007\/978-3-540-27836-8_11"},{"volume-title":"Proceedings of the 12th Mediterranean Electrotechnical Conference.","author":"de Renesse R.","key":"e_1_2_1_34_1","unstructured":"de Renesse , R. and Aghvami , A. H . 2004. Formal verification of ad hoc routing protocols using spin model checker . In Proceedings of the 12th Mediterranean Electrotechnical Conference. de Renesse, R. and Aghvami, A. H. 2004. Formal verification of ad hoc routing protocols using spin model checker. In Proceedings of the 12th Mediterranean Electrotechnical Conference."},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"de Souza e Silva E. and Gail H. 2000. Transient Solutions for Markov Chains. In W. Grassmann Ed. Kluwer Dordrecht The Netherlands.  de Souza e Silva E. and Gail H. 2000. Transient Solutions for Markov Chains. In W. Grassmann Ed. Kluwer Dordrecht The Netherlands.","DOI":"10.1007\/978-1-4757-4828-4_3"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Doucet A. de Freitas N. and Gordon N. 2001. Sequential Monte Carlo Methods in Practice. John Wiley and Sons New York NY.  Doucet A. de Freitas N. and Gordon N. 2001. Sequential Monte Carlo Methods in Practice. John Wiley and Sons New York NY.","DOI":"10.1007\/978-1-4757-3437-9"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-003-0042-x"},{"volume-title":"Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 415--425","author":"Elwalid A. I.","key":"e_1_2_1_38_1","unstructured":"Elwalid , A. I. and Mitra , D . 1992. Fluid models for the analysis and design of statistical multiplexing with loss priorities on multiple classes of bursty traffic . In Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 415--425 . Elwalid, A. I. and Mitra, D. 1992. Fluid models for the analysis and design of statistical multiplexing with loss priorities on multiple classes of bursty traffic. In Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 415--425."},{"volume-title":"Temporal and Modal Logic","author":"Emerson E. A.","key":"e_1_2_1_39_1","unstructured":"Emerson , E. A. 1990. Temporal and Modal Logic . MIT Press , Cambridge, MA . Emerson, E. A. 1990. Temporal and Modal Logic. MIT Press, Cambridge, MA."},{"volume-title":"Proceedings of the 5th International Conference on Verification, Model checking and Abstract Interpretation. 191--210","author":"Engler D.","key":"e_1_2_1_40_1","unstructured":"Engler , D. and Musuvathi , M . 2004. Static analysis versus software model checking for bug finding . In Proceedings of the 5th International Conference on Verification, Model checking and Abstract Interpretation. 191--210 . Engler, D. and Musuvathi, M. 2004. Static analysis versus software model checking for bug finding. In Proceedings of the 5th International Conference on Verification, Model checking and Abstract Interpretation. 191--210."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00867-2_1"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/2090188.2090204"},{"key":"e_1_2_1_43_1"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1288107.1288114"},{"volume-title":"Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 206--210","author":"Garetto M.","key":"e_1_2_1_45_1","unstructured":"Garetto , M. , Giaccone , P. , and Leonardi , E . 2008a. Capacity scaling of sparse mobile ad hoc networks . In Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 206--210 . Garetto, M., Giaccone, P., and Leonardi, E. 2008a. Capacity scaling of sparse mobile ad hoc networks. In Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 206--210."},{"volume-title":"Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 1--13","author":"Garetto M.","key":"e_1_2_1_46_1","unstructured":"Garetto , M. , Salonidis , T. , and Knightly , E . 2006. Modeling per-flow throughput and capturing starvation in CSMA multi-hop wireless networks . In Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 1--13 . Garetto, M., Salonidis, T., and Knightly, E. 2006. Modeling per-flow throughput and capturing starvation in CSMA multi-hop wireless networks. In Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 1--13."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2007.902687"},{"volume-title":"Proceedings of USENIX General Track.","author":"Girod L.","key":"e_1_2_1_48_1","unstructured":"Girod , L. , Elson , J. , Cerpa , A. , Stathopoulos , T. , Ramanathan , N. , and Estrin , D . 2004a. Emstar: A software environment for developing and deploying wireless sensor networks . In Proceedings of USENIX General Track. Girod, L., Elson, J., Cerpa, A., Stathopoulos, T., Ramanathan, N., and Estrin, D. 2004a. Emstar: A software environment for developing and deploying wireless sensor networks. In Proceedings of USENIX General Track."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1031495.1031519"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.009"},{"volume-title":"Proceedings of the 1st Forum on Specification and Design Languages (FDL).","author":"Godary K.","key":"e_1_2_1_51_1","unstructured":"Godary , K. , Aug\u00e9-Blum , I. , and Mignotte , A . 2004. Sdl and timed Petri nets versus uppaal for the validation of embedded architecture in automative . In Proceedings of the 1st Forum on Specification and Design Languages (FDL). Godary, K., Aug\u00e9-Blum, I., and Mignotte, A. 2004. Sdl and timed Petri nets versus uppaal for the validation of embedded architecture in automative. In Proceedings of the 1st Forum on Specification and Design Languages (FDL)."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2002.801403"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0059-8"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1364782.1364788"},{"key":"e_1_2_1_59_1","unstructured":"HOL. 2005. http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL\/.  HOL. 2005. http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/HOL\/."},{"volume-title":"Design and Validation of Computer Networks","author":"Holzmann G. J.","key":"e_1_2_1_60_1","unstructured":"Holzmann , G. J. 1991. Design and Validation of Computer Networks . Prentice-Hall International Editions , Englewood Cliffs, NJ . Holzmann, G. J. 1991. Design and Validation of Computer Networks. Prentice-Hall International Editions, Englewood Cliffs, NJ."},{"volume-title":"The SPIN Model Checker","author":"Holzmann G. J.","key":"e_1_2_1_61_1","unstructured":"Holzmann , G. J. 2003. The SPIN Model Checker . Addison-Wesley, Reading , MA. Holzmann, G. J. 2003. The SPIN Model Checker. Addison-Wesley, Reading, MA."},{"volume-title":"Message Sequence Charts (MSC'96). ITU-T","key":"e_1_2_1_62_1","unstructured":"ITU-T 1996. Message Sequence Charts (MSC'96). ITU-T , Geneva, Switzerland . ITU-T 1996. Message Sequence Charts (MSC'96). ITU-T, Geneva, Switzerland."},{"key":"e_1_2_1_63_1","unstructured":"Jacobson I. Booch G. and Rumbaugh J. 1999. The Unified Software Development Process. Addison-Wesley Reading MA.   Jacobson I. Booch G. and Rumbaugh J. 1999. The Unified Software Development Process. Addison-Wesley Reading MA."},{"key":"e_1_2_1_64_1","unstructured":"Javier E. and Raymond P. 2005. The lucky language reference manual. Tech. rep. TR-2004-06 Verimag Gi\u00e9res France.  Javier E. and Raymond P. 2005. The lucky language reference manual. Tech. rep. TR-2004-06 Verimag Gi\u00e9res France."},{"key":"e_1_2_1_65_1","unstructured":"Jeffries R. and Ambler S. W. 2002. Agile Modeling. Jon Wiley &amp; Sons New York NY.  Jeffries R. and Ambler S. W. 2002. Agile Modeling. Jon Wiley &amp; Sons New York NY."},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of the 2nd European Workshop on Model Driven Architecture with an emphasis on Methodologies and Transformations. 28--35","author":"Jones V.","year":"2004","unstructured":"Jones , V. , Rensink , A. , Ruys , T. , Brinksma , E. , and van Halteren , A. 2004 . A formal MDA approach for mobile health systems . In Proceedings of the 2nd European Workshop on Model Driven Architecture with an emphasis on Methodologies and Transformations. 28--35 . Jones, V., Rensink, A., Ruys, T., Brinksma, E., and van Halteren, A. 2004. A formal MDA approach for mobile health systems. In Proceedings of the 2nd European Workshop on Model Driven Architecture with an emphasis on Methodologies and Transformations. 28--35."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/894210"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.adhoc.2005.12.003"},{"volume-title":"Proceedings of the 11th Euromicro Conference on Real-Time Systems. 1--14","author":"Kim M.","key":"e_1_2_1_69_1","unstructured":"Kim , M. , Viswanathan , M. , Ben-Abdallah , H. , Kannan , S. , Lee , I. , and Sokolsky , O . 1999. Formally specified monitoring of temporal properties . In Proceedings of the 11th Euromicro Conference on Real-Time Systems. 1--14 . Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., and Sokolsky, O. 1999. Formally specified monitoring of temporal properties. In Proceedings of the 11th Euromicro Conference on Real-Time Systems. 1--14."},{"key":"e_1_2_1_70_1","first-page":"268","article-title":"Safety and liveness properties: A survey","volume":"53","author":"Kindler E.","year":"1994","unstructured":"Kindler , E. 1994 . Safety and liveness properties: A survey . Bull. Eur. Assoc. Theor. Comput. Sci. 53 , 268 -- 272 . Kindler, E. 1994. Safety and liveness properties: A survey. Bull. Eur. Assoc. Theor. Comput. Sci. 53, 268--272.","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci."},{"volume-title":"Queueing Systems","author":"Kleinrock L.","key":"e_1_2_1_71_1","unstructured":"Kleinrock , L. 1975. Queueing Systems . Wiley-Interscience , New York, NY . Kleinrock, L. 1975. Queueing Systems. Wiley-Interscience, New York, NY."},{"volume-title":"Proceedings of the 2nd International Conference on Testbeds and Research Infrastructures for the Development of Networks and Communities (TRIDENTCOM).","author":"Kropff M.","key":"e_1_2_1_72_1","unstructured":"Kropff , M. , Krop , T. , Hollick , M. , Mogre , P. S. , and Steinmetz , R . 2006. A survey on real world and emulation testbeds for mobile ad hoc networks . In Proceedings of the 2nd International Conference on Testbeds and Research Infrastructures for the Development of Networks and Communities (TRIDENTCOM). Kropff, M., Krop, T., Hollick, M., Mogre, P. S., and Steinmetz, R. 2006. A survey on real world and emulation testbeds for mobile ad hoc networks. In Proceedings of the 2nd International Conference on Testbeds and Research Infrastructures for the Development of Networks and Communities (TRIDENTCOM)."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1096166.1096174"},{"volume-title":"In Proceedings of the 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS).","author":"Kwiatkowska M.","key":"e_1_2_1_74_1","unstructured":"Kwiatkowska , M. , Norman , G. , and Parker , D . 2005. Probabilistic model checking and power-aware computing . In In Proceedings of the 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS). Kwiatkowska, M., Norman, G., and Parker, D. 2005. Probabilistic model checking and power-aware computing. In In Proceedings of the 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS)."},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00046-9"},{"volume-title":"Proceedings of the 2nd Joint International Workshop on Process Algebra and Probabilitics Methods, Performance Modeling and Verification. 169--187","author":"Kwiatkowska M.","key":"e_1_2_1_76_1","unstructured":"Kwiatkowska , M. , Norman , G. , and Sproston , J . 2002b. Probabilitic model checking of the ieee 802.11 wireless local area network protocol . In Proceedings of the 2nd Joint International Workshop on Process Algebra and Probabilitics Methods, Performance Modeling and Verification. 169--187 . Kwiatkowska, M., Norman, G., and Sproston, J. 2002b. Probabilitic model checking of the ieee 802.11 wireless local area network protocol. In Proceedings of the 2nd Joint International Workshop on Process Algebra and Probabilitics Methods, Performance Modeling and Verification. 169--187."},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/NCM.2008.248"},{"key":"e_1_2_1_79_1","unstructured":"Lahiri S. K. and Bryant R. E. 2005. UCLID-PA homepage: Verification tool for UCLID models using predicate abstraction. Carnegie Mellon University Pittsburgh PA.  Lahiri S. K. and Bryant R. E. 2005. UCLID-PA homepage: Verification tool for UCLID models using predicate abstraction. Carnegie Mellon University Pittsburgh PA."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297662"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"volume-title":"Proceedings of the International Teletraffic Congress. 1101--1112","author":"Leao R. M. M.","key":"e_1_2_1_82_1","unstructured":"Leao , R. M. M. , de Souza e Silva, E., and Diniz , M. C . 2001. Traffic engineering using reward models . In Proceedings of the International Teletraffic Congress. 1101--1112 . Leao, R. M. M., de Souza e Silva, E., and Diniz, M. C. 2001. Traffic engineering using reward models. In Proceedings of the International Teletraffic Congress. 1101--1112."},{"volume-title":"Proceedings of the IEEE Wireless Communications and Networking Conf. (WCNC). 1162--1167","author":"Lin T.","key":"e_1_2_1_83_1","unstructured":"Lin , T. , Midkiff , S. , and Park , J . 2003. A framework for wireless ad hoc routing protocols . In Proceedings of the IEEE Wireless Communications and Networking Conf. (WCNC). 1162--1167 . Lin, T., Midkiff, S., and Park, J. 2003. A framework for wireless ad hoc routing protocols. In Proceedings of the IEEE Wireless Communications and Networking Conf. (WCNC). 1162--1167."},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/570790.570799"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2007.10.031"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/1163653.1163663"},{"key":"e_1_2_1_87_1","first-page":"34","article-title":"A step-wise validation approach for a wireless routing protocol","volume":"1","author":"Maag S.","year":"2007","unstructured":"Maag , S. and Zaidi , F. 2007 . A step-wise validation approach for a wireless routing protocol . Posts, Telecomm. Inform. Tech. J. 1 , 34 -- 40 . Maag, S. and Zaidi, F. 2007. A step-wise validation approach for a wireless routing protocol. Posts, Telecomm. Inform. Tech. J. 1, 34--40.","journal-title":"Posts, Telecomm. Inform. Tech. J."},{"key":"e_1_2_1_88_1","doi-asserted-by":"crossref","unstructured":"Macker J. P. Chao W. and Weston J. W. 2003. A low-cost IP-based mobile network emulator (MNE). Tech. rep. ADA464904. Naval Research Lab Washington D.C.  Macker J. P. Chao W. and Weston J. W. 2003. A low-cost IP-based mobile network emulator (MNE). Tech. rep. ADA464904. Naval Research Lab Washington D.C.","DOI":"10.21236\/ADA464904"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069782"},{"key":"e_1_2_1_90_1","doi-asserted-by":"crossref","unstructured":"Manna Z. Bj\u00f8rner N. S. Browne A. Col\u00f3n M. Finkbeiner B. Pichora M. Sipma H. B. and Uribe T. E. 1999. An update on STeP: Deductive-algorithmic verification of reactive systems. In Tool Support for System Specification Development and Verification R. Berghammer and Y. Lakhnech Eds. Advances in Computing Science. Springer-Verlag Berlin Germany 174--188.  Manna Z. Bj\u00f8rner N. S. Browne A. Col\u00f3n M. Finkbeiner B. Pichora M. Sipma H. B. and Uribe T. E. 1999. An update on STeP: Deductive-algorithmic verification of reactive systems. In Tool Support for System Specification Development and Verification R. Berghammer and Y. Lakhnech Eds. Advances in Computing Science. Springer-Verlag Berlin Germany 174--188.","DOI":"10.1007\/978-3-7091-6355-9_13"},{"volume-title":"Extension of the Limit Theorems of Probability Theory to a Sum of Variables Connected in a Chain. Markov Chains","author":"Markov A.","key":"e_1_2_1_91_1","unstructured":"Markov , A. 1971. Extension of the Limit Theorems of Probability Theory to a Sum of Variables Connected in a Chain. Markov Chains . John Wiley and Sons , New York, NY . Markov, A. 1971. Extension of the Limit Theorems of Probability Theory to a Sum of Variables Connected in a Chain. Markov Chains. John Wiley and Sons, New York, NY."},{"volume-title":"Rapid Application Development","author":"Martin J.","key":"e_1_2_1_92_1","unstructured":"Martin , J. 1990. RAD , Rapid Application Development . MacMillan Publishing Co , New York, NY . Martin, J. 1990. RAD, Rapid Application Development. MacMillan Publishing Co, New York, NY."},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1007\/11921240_4"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.51"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICWMC.2007.2"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(99)00061-4"},{"key":"e_1_2_1_97_1","doi-asserted-by":"crossref","unstructured":"Perkins C. Belding-Royer E. and Das S. 2003. Rfc 3561: ad hoc on-demand distance vector (AODV) routing. IETF Tech. rep. www.ietf.org.   Perkins C. Belding-Royer E. and Das S. 2003. Rfc 3561: ad hoc on-demand distance vector (AODV) routing. IETF Tech. rep. www.ietf.org.","DOI":"10.17487\/rfc3561"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/356698.356702"},{"volume-title":"Petri Net Theory and the Modeling of Systems","author":"Peterson J. L.","key":"e_1_2_1_99_1","unstructured":"Peterson , J. L. 1981. Petri Net Theory and the Modeling of Systems . Prentice Hall, Englewood Cliffs , NJ. Peterson, J. L. 1981. Petri Net Theory and the Modeling of Systems. Prentice Hall, Englewood Cliffs, NJ."},{"volume-title":"Proceedings of the 12th International Conference on Performance Evaluation: Modelling Techniques and Tools. Springer Verlag","author":"Petriu D.","key":"e_1_2_1_101_1","unstructured":"Petriu , D. and Woodside , M . 2002. Software performance models from systems scenarios in use case maps . In Proceedings of the 12th International Conference on Performance Evaluation: Modelling Techniques and Tools. Springer Verlag , Berlin, Germany, 1--8. Petriu, D. and Woodside, M. 2002. Software performance models from systems scenarios in use case maps. In Proceedings of the 12th International Conference on Performance Evaluation: Modelling Techniques and Tools. Springer Verlag, Berlin, Germany, 1--8."},{"volume-title":"Proceedings of the 4th International Conf. on Testbeds and Research Infrastructures for the Development of Networks and Communities (TRIDENTCOM).","author":"Pizzonia M.","key":"e_1_2_1_102_1","unstructured":"Pizzonia , M. and Rimondini , M . 2008. Easy emulation of complex networks on inexpensive hardware . In Proceedings of the 4th International Conf. on Testbeds and Research Infrastructures for the Development of Networks and Communities (TRIDENTCOM). Pizzonia, M. and Rimondini, M. 2008. Easy emulation of complex networks on inexpensive hardware. In Proceedings of the 4th International Conf. on Testbeds and Research Infrastructures for the Development of Networks and Communities (TRIDENTCOM)."},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.99196"},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"e_1_2_1_105_1","volume-title":"NEMAN: A network emulator for mobile ad-hoc networks. Tech. rep. TR321. Department of Informatcis","author":"Puzar M.","year":"2005","unstructured":"Puzar , M. and Plagemann , T . 2005 . NEMAN: A network emulator for mobile ad-hoc networks. Tech. rep. TR321. Department of Informatcis , University of Oslo , Oslo, Norway . Puzar, M. and Plagemann, T. 2005. NEMAN: A network emulator for mobile ad-hoc networks. Tech. rep. TR321. Department of Informatcis, University of Oslo, Oslo, Norway."},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comcom.2004.07.024"},{"volume-title":"Emulation of computer networks with Netkit. Tech. rep. TR RT-DIA-113-2007","author":"Rimondini M.","key":"e_1_2_1_107_1","unstructured":"Rimondini , M. 2007. Emulation of computer networks with Netkit. Tech. rep. TR RT-DIA-113-2007 . University of Roma Tre , Rome, Italy . Rimondini, M. 2007. Emulation of computer networks with Netkit. Tech. rep. TR RT-DIA-113-2007. University of Roma Tre, Rome, Italy."},{"key":"e_1_2_1_108_1","volume-title":"Proceedings of the International Conference on Software Engineering Table of Contents. 328--338","author":"Royce W. W.","year":"1987","unstructured":"Royce , W. W. 1987 . Managing the development of large software systems: concepts and techniques . In Proceedings of the International Conference on Software Engineering Table of Contents. 328--338 . Royce, W. W. 1987. Managing the development of large software systems: concepts and techniques. In Proceedings of the International Conference on Software Engineering Table of Contents. 328--338."},{"key":"e_1_2_1_109_1","doi-asserted-by":"crossref","unstructured":"Rubinstein R. Y. and Kroese D. P. 2007. Simulation and the Monte Carlo Method. John Wiley &amp; Sons New York NY.   Rubinstein R. Y. and Kroese D. P. 2007. Simulation and the Monte Carlo Method. John Wiley &amp; Sons New York NY.","DOI":"10.1002\/9780470230381"},{"key":"e_1_2_1_110_1","doi-asserted-by":"crossref","unstructured":"Rutten J. M.Kwiatkowska Norman G. and Parker D. 2004. Mathematical techniques for analysing concurrent and probabilitics systems. CRM Monograph Series 23. American Mathematical Society Providence RI.  Rutten J. M.Kwiatkowska Norman G. and Parker D. 2004. Mathematical techniques for analysing concurrent and probabilitics systems. CRM Monograph Series 23. American Mathematical Society Providence RI.","DOI":"10.1090\/crmm\/023"},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142680.1142684"},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICASSP.2000.860212"},{"key":"e_1_2_1_113_1","unstructured":"Spivey J. M. and Spivey M. 1996. An Introduction to Logic Programming Through Prolog. Prentice Hall Englewood Cliffs NJ.   Spivey J. M. and Spivey M. 1996. An Introduction to Logic Programming Through Prolog. Prentice Hall Englewood Cliffs NJ."},{"volume-title":"Proceedings of SDL'97","author":"Steppler M.","key":"e_1_2_1_114_1","unstructured":"Steppler , M. and Lott , M . 1997. Speet\u2014SDL performance evaluation tool . In Proceedings of SDL'97 . 53--67. Steppler, M. and Lott, M. 1997. Speet\u2014SDL performance evaluation tool. In Proceedings of SDL'97. 53--67."},{"key":"e_1_2_1_115_1","unstructured":"Sterling L. and Shapiro E. 1994. The Art of Prolog. MIT Press Cambridge MA.  Sterling L. and Shapiro E. 1994. The Art of Prolog. MIT Press Cambridge MA."},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019125015943"},{"volume-title":"Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 7--11","author":"Tickoo O.","key":"e_1_2_1_117_1","unstructured":"Tickoo , O. and Sikdar , B . 2004. Queueing analysis and delay mitigation in IEEE 802.11 random access MAC based wireless networks . In Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 7--11 . Tickoo, O. and Sikdar, B. 2004. Queueing analysis and delay mitigation in IEEE 802.11 random access MAC based wireless networks. In Proceedings of the Annual Joint Conference of the IEEE Computer and Communications Societies. 7--11."},{"key":"e_1_2_1_118_1","unstructured":"Vahdat A. and Becker D. 2000. Epidemic routing for partially-connected ad hoc networks. Tech. rep. Duke University Durham NC.  Vahdat A. and Becker D. 2000. Epidemic routing for partially-connected ad hoc networks. Tech. rep. Duke University Durham NC."},{"key":"e_1_2_1_119_1","unstructured":"Verilog. 1997. ObjectGEODE Simulator.  Verilog. 1997. ObjectGEODE Simulator."},{"key":"e_1_2_1_120_1","volume-title":"Sotware Engineering: Principles and Practice","author":"Vliet H. V.","year":"1999","unstructured":"Vliet , H. V. 1999 . Sotware Engineering: Principles and Practice ( 2 nd Edition). Wiley , New York, NY . Vliet, H. V. 1999. Sotware Engineering: Principles and Practice (2nd Edition). Wiley, New York, NY.","edition":"2"},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDCAT.2005.168"},{"key":"e_1_2_1_122_1","volume-title":"Tech. Rep. 5782, RR-5782. INRIA","author":"Watteyne T.","year":"2005","unstructured":"Watteyne , T. , Auge-Blum , I. , and Ubeda , S . 2005 . Formal QoS validation approach on a real-time MAC protocol for wireless sensor networks. Tech. Rep. 5782, RR-5782. INRIA , Rocquencourt, France . Watteyne, T., Auge-Blum, I., and Ubeda, S. 2005. Formal QoS validation approach on a real-time MAC protocol for wireless sensor networks. Tech. Rep. 5782, RR-5782. INRIA, Rocquencourt, France."},{"volume-title":"Proceedings of SDL 2003: System Design","author":"Wei M.","key":"e_1_2_1_123_1","unstructured":"Wei , M. , Dubois , F. , Vincent , D. , and Combes , P . 2003. Looking for better integration of design and performance engineering . In Proceedings of SDL 2003: System Design , Springer, Berlin, Germany, 1--17. Wei, M., Dubois, F., Vincent, D., and Combes, P. 2003. Looking for better integration of design and performance engineering. In Proceedings of SDL 2003: System Design, Springer, Berlin, Germany, 1--17."},{"key":"e_1_2_1_125_1","doi-asserted-by":"publisher","DOI":"10.1145\/1031495.1031498"},{"key":"e_1_2_1_126_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529284"},{"key":"e_1_2_1_127_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.07.009"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1883612.1883614","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1883612.1883614","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:17Z","timestamp":1750243937000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1883612.1883614"}},"subtitle":["Linking wireless self-organizing network validation techniques with formal testing approaches"],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":122,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1145\/1883612.1883614"],"URL":"https:\/\/doi.org\/10.1145\/1883612.1883614","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"type":"print","value":"0360-0300"},{"type":"electronic","value":"1557-7341"}],"subject":[],"published":{"date-parts":[[2011,1]]},"assertion":[{"value":"2008-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-02-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}