E. Es, Methods for testing and specification (mts); the testing and test control notation version 3; part 1: Ttcn-3 core language, pp.873-874, 2007.

F. B. Abdesslem, L. Iannone, K. Obraczka, M. D. De-amorim, I. Solis et al., A Prototyping Environment for Wireless Multihop Networks, Proc. of AINTEC, pp.38-43, 2007.
DOI : 10.1007/978-3-540-76809-8_4
URL : https://hal.archives-ouvertes.fr/hal-01311771

R. Alur and D. Dill, Automata for modeling real-time systems, Internation Colloquium on Automata, Languages and Programming, pp.321-335, 1990.
DOI : 10.1007/BFb0032042

T. R. Andel and A. Yasinsac, On the Credibility of Manet Simulations, Computer, vol.39, issue.7, pp.48-54, 2006.
DOI : 10.1109/MC.2006.242

R. M. Le-ao, E. De-souza-e-silva, and M. C. Diniz, Traffic engineering using reward models, Proc. of the International Teletraffic Congress, pp.1101-1112, 2001.

R. Bagrodia and M. Takai, Position paper on validation of network simulation models, DARPA/NIST Network Simulation Validation Workshop, 1999.

O. Balci, Verification validation and accreditation of simulation models, Proceedings of the 29th conference on Winter simulation , WSC '97, pp.135-141
DOI : 10.1145/268437.268462

P. Ballarini and A. Miller, (towards) model checking medium access control for sensor networks, Proc. of the 2nd IEEE international symposium on leveraging applications of formal methods, pp.256-262, 2006.
DOI : 10.1109/isola.2006.16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.9125

E. Bayse, A. Cavalli, M. Núñez, and F. Zaïdi, A passive testing approach based on invariants: application to the WAP, Computer Networks, vol.48, issue.2, pp.247-266, 2005.
DOI : 10.1016/j.comnet.2004.09.009

F. Benbadis, M. D. De-amorim, and S. Fdida, ELIP: Embedded Location Information Protocol, IFIP Networking, 2005.
DOI : 10.1007/11422778_93
URL : https://hal.archives-ouvertes.fr/hal-01487874

K. Bhargavan, D. Obradovic, and C. A. Gunter, Formal verification of standards for distance vector routing protocols, Journal of the ACM, vol.49, issue.4, pp.538-576, 2002.
DOI : 10.1145/581771.581775

K. Bhargavan, C. A. Gunter, M. Kim, I. Lee, D. Obradovic et al., Verisim: formal analysis of network simulations, IEEE Transactions on Software Engineering, vol.28, issue.2, pp.129-145, 2002.
DOI : 10.1109/32.988495

G. Bianchi, Performance analysis of the IEEE 802.11 distributed coordination function, IEEE Journal on Selected Areas in Communications, vol.18, issue.3, pp.535-547, 2000.
DOI : 10.1109/49.840210

B. Boehms, A spiral model of software development and enhancement, IEEE Computer, pp.61-72, 1988.

G. Bolch, S. Greiner, H. De-meer, and K. S. Trivedi, Queueing Networks and Markov Chains, 2006.
DOI : 10.1002/0471791571

R. Boorstyn, A. Kershenbaum, B. Maglaris, and V. Sahin, Throughput Analysis in Multihop CSMA Packet Radio Networks, IEEE Transactions on Communications, vol.35, issue.3, pp.267-274, 1987.
DOI : 10.1109/TCOM.1987.1096769

M. M. Borujerdi and S. M. Mirzababaei, Formal verification of a multicast protocol in mobile networks, International Journal of Signal Processing, vol.1, issue.4, pp.212-218, 2004.

M. Bütow, M. Mestern, C. Schapiro, and P. S. Kritzinger, Performance Modelling with the Formal Specification Language SDL, INRIA Linking Wireless Self-Organizing Networks Validation Techniques with Formal Testing approaches35 IFIP TC6/ 6.1 the 16th international conference on formal description techniques IX/protocol specification , testing and verification XVI on Formal description techniques IX : theory, application and tools, pp.213-228, 1996.
DOI : 10.1007/978-0-387-35079-0_13

A. Cavalli, A. Mederreg, F. Zaïdi, P. Combes, W. Monin et al., A Multi-service and Multi-protocol Validation Platform ??? Experimentation Results, The 16th IFIP International Conference on Testing of Communication Systems, pp.17-32, 2004.
DOI : 10.1007/978-3-540-24704-3_2
URL : https://hal.archives-ouvertes.fr/hal-00118074

D. Cavin, Y. Sasson, and A. Schiper, On the accuracy of MANET simulators, Proceedings of the second ACM international workshop on Principles of mobile computing , POMC '02, pp.38-43, 2002.
DOI : 10.1145/584490.584499

C. Chaudet, I. G. Lassous, E. Thierry, and B. Gaujal, Study of the impact of asymmetry and carrier sense mechanism in ieee 802.11 multihops networks through a basic case, Proc. of the 1st ACM international workshop on Performance evaluation of wireless ad hoc, sensor, and ubiquitous networks, pp.1-7, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00100142

S. Chiyangwa and M. Kwiatkowska, A Timing Analysis of AODV, Proc. 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-based Distributed Systems, pp.306-321, 2005.
DOI : 10.1007/978-3-540-30232-2_22

D. Christmann, P. Becker, R. Gotzhein, and T. Kuhn, Model-driven development of a mac layer for ad-hoc networks with sdl, Proc. of 1st Workshop on "ITU System Design Languages, 2008.

E. M. Clarke and E. A. Emerson, Synthesis of synchronization skeletons for branching time temporal logic, Proc. 1st Workshop on Logic of Programs, 1981.

E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking, 1999.

J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Puasuareanu et al., Bandera, Proceedings of the 22nd international conference on Software engineering , ICSE '00, pp.439-448, 2000.
DOI : 10.1145/337180.337234

D. Curren, A survey of simulation in sensor networks, 2005.

A. P. Da-silva, R. M. Leäo, E. De-souza-e, and . Silva, An efficient approximate technique for solving fluid models, ACM SIGMETRICS Performance Evaluation Review, vol.32, issue.2, pp.6-8, 2004.
DOI : 10.1145/1035334.1035338

A. Silva, Computational Methods for Markov Reward Models, 2006.

S. Das and D. L. Dill, Counter-Example Based Predicate Discovery in Predicate Abstraction, Proc. 4th International Conference on Formal Methods in Computer-Aided Design, pp.19-32, 2002.
DOI : 10.1007/3-540-36126-X_2

R. De-renesse and A. H. Aghvami, Formal verification of ad-hoc routing protocols using SPIN model checker, Proceedings of the 12th IEEE Mediterranean Electrotechnical Conference (IEEE Cat. No.04CH37521), 2004.
DOI : 10.1109/MELCON.2004.1348275

E. De-souza-e-silva and H. R. Gail, Transient Solutions for Markov Chains, Computational Probability, Kluwer, 2000.
DOI : 10.1007/978-1-4757-4828-4_3

. Deterlab, Network security testbed, www.deterlab.net

A. Doucet, N. Nando-de-freitas, and . Gordon, Sequential Monte Carlo methods in practice, 2001.
DOI : 10.1007/978-1-4757-3437-9

E. Nordström, DSR-UU v0.1. http://core.it.uu.se/core/index

C. Eisner, Formal verification of software source code through semi-automatic modelling, Software and System Modelling, pp.14-31, 2005.

I. Anwar, D. Elwalid, and . Mitra, Fluid models for the analysis and design of statistical multiplexing with loss priorities on multiple classes of bursty traffic

E. A. Emerson, Temporal and Modal Logic, 42] EmStar. Software for Wireless Sensor Networks, 1990.
DOI : 10.1016/B978-0-444-88074-1.50021-4

. Emulab, Total network testbed, www.emulab.net

D. Engler and M. Musuvathi, Static Analysis versus Software Model Checking for Bug Finding, Proc. 5th International Conference on Verification, Model checking and Abstract Interpretation, pp.191-210, 2004.
DOI : 10.1007/978-3-540-24622-0_17

A. Fehnker, M. Fruth, and A. Mciver, Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols, Proceedings of the Workshop on Methods, Models and Tools for Fault Tolerance (MeMoT 2007) at the 7th International Conference on Integrated Formal Methods, pp.80-87, 2007.
DOI : 10.1007/978-3-540-24730-2_4

M. J. Fernández-iglesias, J. C. Burguillo-rial, and F. J. No, Wireless protocol testing and validation supported by formal methods. A hands-on report, Journal of Systems and Software, vol.75, issue.1-2, pp.139-154, 2005.
DOI : 10.1016/j.jss.2004.03.001

M. Garetto, P. Giaccone, and E. Leonardi, Capacity scaling in delay tolerant networks with heterogeneous mobile nodes, Proceedings of the 8th ACM international symposium on Mobile ad hoc networking and computing , MobiHoc '07, pp.15-17, 2007.
DOI : 10.1145/1288107.1288114

M. Garetto, P. Giaccone, and E. Leonardi, Capacity Scaling of Sparse Mobile Ad Hoc Networks, IEEE INFOCOM 2008, The 27th Conference on Computer Communications, pp.206-210, 2008.
DOI : 10.1109/INFOCOM.2008.50

M. Garetto, T. Salonidis, and E. Knightly, Modeling per-flow throughput and capturing starvation in csma multi-hop wireless networks, Proc. of IEEE INFOCOM, pp.1-13, 2006.

M. Garetto, T. Salonidis, and E. W. Knightly, Modeling Per-Flow Throughput and Capturing Starvation in CSMA Multi-Hop Wireless Networks, IEEE/ACM Transactions on Networking, vol.16, issue.4, pp.864-877, 2008.
DOI : 10.1109/TNET.2007.902687

L. Girod, J. Elson, A. Cerpa, T. Stathopoulos, N. Ramanathan et al., Emstar, Proc. of USENIX General Track, 2004.
DOI : 10.1145/1267060.1267061

L. Girod, T. Stathopoulos, N. Ramanathan, J. Elson, D. Estrin et al., A system for simulation, emulation, and deployment of heterogeneous sensor networks, Proceedings of the 2nd international conference on Embedded networked sensor systems , SenSys '04, 2004.
DOI : 10.1145/1031495.1031519

U. Glässer and Q. Gu, Formal description and analysis of a distributed location service for mobile ad hoc networks, Theoretical Computer Science, vol.336, issue.2-3, pp.285-309, 2005.
DOI : 10.1016/j.tcs.2004.11.009

K. Godary, I. Augé-blum, and A. Mignotte, Sdl and timed petri nets versus uppaal for the validation of embedded architecture in automative, Proc. 1st Forum on Specification and Design Languages (FDL), 2004.

P. Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.174-186, 1997.
DOI : 10.1145/263699.263717

M. Grossglauser and D. Tse, Mobility increases the capacity of ad hoc wireless networks, IEEE/ACM Transactions on Networking, vol.10, issue.4, pp.477-486, 2002.
DOI : 10.1109/TNET.2002.801403

E. Gunter and D. Peled, Model checking, testing and verification working together, Formal Aspects of Computing, vol.17, issue.2, pp.201-221, 2005.
DOI : 10.1007/s00165-005-0059-8

K. Havelund and T. Pressburger, Model checking java programs using java pathfinder. Software Tools for Technology Transfer, pp.366-381, 2000.
DOI : 10.1007/s100090050043
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.7274

E. Heck, Performance Evaluation of Formally Specified Systems -the intergration of SDL with HIT, 1996.

L. Hoffman, In search of dependable design, Communications of the ACM, vol.51, issue.7, pp.14-16, 2008.
DOI : 10.1145/1364782.1364788

G. J. Holzmann, Design and Validation of Computer Networks, 1991.

G. J. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, 2003.
DOI : 10.1109/32.588521

E. Javier and P. Raymond, The lucky language reference manual, 2005.

R. Jeffries and S. W. Ambler, Agile Modeling, 2002.

V. Jones, A. Rensink, T. Ruys, E. Brinksma, and A. Van-halteren, A formal mda approach for mobile health systems, Proc. of the 2nd European Workshop on Model Driven Architecture with an emphasis on Methodologies and Transformations, pp.28-35, 2004.

S. Keshav, Real:a network simulator, 1988.

W. Kiess and M. Mauve, A survey on real-world implementations of mobile ad-hoc networks, Ad Hoc Networks, 2007.
DOI : 10.1016/j.adhoc.2005.12.003

W. Kiess and M. Mauvea, A survey on real-world implementations of mobile ad-hoc networks, Ad Hoc Networks, pp.538-576, 2007.
DOI : 10.1016/j.adhoc.2005.12.003

M. Kim, M. Viswanathan, H. Ben-abdallah, S. Kannan, I. Lee et al., Formally specified monitoring of temporal properties, Proc. 11th Euromicro Conference on Real-Time Systems, pp.1-14, 1999.

E. Kindler, Safety and liveness properties: A survey, Bulletin of the European Association for Theoretical Computer Science, issue.53, pp.268-272, 1994.

L. Kleinrock, Queueing Systems, 1975.

M. Kropff, T. Krop, M. Hollick, P. S. Mogre, and R. Steinmetz, A survey on real world and emulation testbeds for mobile ad hoc networks, Proc. 2nd International Conference on Testbeds and Research Infrastructures for the Development of Networks and Communities (TRIDENTCOM), 2006.

S. Kurkowski, T. Camp, and M. Colagrosso, MANET simulation studies, ACM SIGMOBILE Mobile Computing and Communications Review, vol.9, issue.4, pp.50-61, 2005.
DOI : 10.1145/1096166.1096174

M. Kwiatkowska, G. Norman, and J. Sproston, Probabilitic model checking of the ieee 802.11 wireless local area network protocol, Proc. 2nd Joint International Workshop on Process Algebra and Probabilitics Methods, Performance Modeling and Verification, pp.169-187, 2002.

J. S. Seok-myun-kwon and . Kim, Coverage ratio in the wireless sensor networks using monte carlo simulation, Proc. of the 4th International Conference on Networked Computing and Advanced Information Management, pp.235-238, 2008.

S. K. Lahiri, Unbounded System Verification Using Decision Procedure and Predicate Abstraction, INRIA Linking Wireless Self-Organizing Networks Validation Techniques with Formal Testing approaches39 [82], 2004.

K. Shuvendu, R. E. Lahiri, and . Bryant, Predicate abstraction with indexed predicates, ACM Transaction on Computational Logic, vol.9, issue.1, p.4, 2007.

K. G. Larsen, P. Petterson, and W. Yi, Uppaal in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152, 1997.
DOI : 10.1007/s100090050010

T. Lin, S. Midkiff, and J. Park, A framework for wireless ad hoc routing protocols, Proc. of IEEE Wireless Communications and Networking Conf. (WCNC), pp.1162-1167, 2003.

H. Lundgren, E. Nordström, and C. Tschudin, Coping with communication gray zones in IEEE 802.11b based ad hoc networks, Proceedings of the 5th ACM international workshop on Wireless mobile multimedia , WOWMOM '02, pp.49-55, 2002.
DOI : 10.1145/570790.570799

S. Maag, C. Grepet, and A. Cavalli, A formal validation methodology for MANET routing protocols based on nodes??? self similarity, Computer Communications, vol.31, issue.4, pp.827-841, 2008.
DOI : 10.1016/j.comcom.2007.10.031
URL : https://hal.archives-ouvertes.fr/hal-01354849

S. Maag and F. Zaidi, Testing methodology for an ad hoc routing protocol, Proceedings of the ACM international workshop on Performance monitoring, measurement, and evaluation of heterogeneous wireless and wired networks , PM2HW2N '06, pp.48-55, 2006.
DOI : 10.1145/1163653.1163663

S. Maag and F. Zaidi, A step-wise validation approach for a wireless routing protocol, Posts, Telecommunications and Information Technology Journal, vol.1, pp.34-40, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01328077

J. P. Macker, W. Chao, and J. W. Weston, A low-cost, IP-based mobile network emulator (MNE), IEEE Military Communications Conference, 2003. MILCOM 2003., 2003.
DOI : 10.1109/MILCOM.2003.1290150

L. Mandel and M. Pouzet, ReactiveML, a reactive extension to ML, Proc. 7th ACM SIGPLAN International conference on Principles and Practice of Declarative Programming (PPDP'05), 2005.
URL : https://hal.archives-ouvertes.fr/hal-01489747

Z. Manna, N. S. Bjørner, A. Browne, M. Colón, B. Finkbeiner et al., An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems, Tool Support for System Specification , Development and Verification, Advances in Computing Science, pp.174-188, 1999.
DOI : 10.1007/978-3-7091-6355-9_13

A. A. Markov, Extension of the limit theorems of probability theory to a sum of variables connected in a chain. Markov Chains, 1971.

J. Martin and . Rad, Rapid Application Development, 1990.

A. Mciver, Quantitative mu-calculus analysis of power management in wireless networks, Proc. 3rd International Theoretical Aspects of Computing, pp.50-64, 2006.

A. K. Mciver and A. Fehnker, Formal Techniques for the Analysis of Wireless Networks, Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (isola 2006), pp.263-270, 2006.
DOI : 10.1109/ISoLA.2006.51

K. Merouane, C. Grepet, and S. Maag, A Methodology for Interoperability Testing of a MANET Routing Protocol, 2007 Third International Conference on Wireless and Mobile Communications (ICWMC'07), 2007.
DOI : 10.1109/ICWMC.2007.2

A. Mitschele-thiel and B. Müller-clostermann, Performance engineering of SDL/MSC systems, Computer Networks, vol.31, issue.17, pp.311801-1816, 1999.
DOI : 10.1016/S1389-1286(99)00061-4

C. Perkins, E. Belding-royer, and S. Das, Rfc 3561, ad hoc on-demand distance vector (aodv) routing, 2003.
DOI : 10.17487/rfc3561

J. Peterson, Petri Nets, ACM Computing Surveys, vol.9, issue.3, pp.223-252, 1977.
DOI : 10.1145/356698.356702

J. Peterson, Petri Net Theory and the Modeling of Systems, 1981.

A. Carl and . Petri, Kommunikation mit Automaten, 1962.

D. Petriu and M. Woodside, Software Performance Models from System Scenarios in Use Case Maps, 12th Int. Performance Evaluation: Modelling Techniques and Tools, pp.1-8, 2002.
DOI : 10.1007/3-540-46029-2_9

M. Pizzonia and M. Rimondini, Netkit: Easy Emulation of Complex Networks on Inexpensive Hardware, Proceedings of the 4th International ICST Conference on Testbeds and Research Infrastructures for the Development of Networks and Communities, 2008.
DOI : 10.4108/tridentcom.2008.3155

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.45-60, 1981.
DOI : 10.1109/SFCS.1977.32

M. Puzar and T. Plagemann, NEMAN: a network emulator for mobile ad-hoc networks, Proceedings of the 8th International Conference on Telecommunications, 2005. ConTEL 2005., 2005.
DOI : 10.1109/CONTEL.2005.185841

S. Ray, D. Starobinski, and J. B. Carruthers, Performance of wireless networks with hidden nodes: a queuing-theoretic analysis, Special Issue on the Performance issues of Wireless LANs, PANs and ad hoc networks, pp.281179-1192, 2005.
DOI : 10.1016/j.comcom.2004.07.024

M. Rimondini, Emulation of computer networks with netkit, 2007.

W. W. Royce, Managing the development of large software systems: concepts and techniques, Proc. of International Conference on Software Engineering Table of Contents, pp.328-338, 1987.

R. Y. Rubinstein and D. P. Kroese, Simulation and the Monte Carlo Method

J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker, Mathematical techniques for analysing concurrent and probabilitics systems, CRM Monograph Series, vol.23, 2004.

S. K. Lahiri and R. E. Bryant, Uclid-pa homepage: Verification tool for uclid models using predicate abstraction, 2005.

L. Samper, F. Maraninchi, L. Mounier, and L. Mandel, GLONEMO, Proceedings of the first international conference on Integrated internet ad hoc and sensor networks , InterSense '06, 2006.
DOI : 10.1145/1142680.1142684

S. A. Sensor, Environment and Network Simulator, osl.cs.uiuc.edu/sens/. [125] SENSE. Sensor Network Simulator and Emulator

. Sensorsim, A Simulation Framework for Sensor Networks, nesl.ee.ucla

M. Sgroi, J. L. Da-silva, F. De-bernardinis, F. Burghardt, A. Sangiovanni-vincentelli et al., Designing wireless protocols: methodology and applications, 2000 IEEE International Conference on Acoustics, Speech, and Signal Processing. Proceedings (Cat. No.00CH37100), pp.3726-3729, 2000.
DOI : 10.1109/ICASSP.2000.860212
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.54

. Simreal, SimReal network simulator

J. M. Spivey and M. Spivey, An Introduction to Logic Programming Through Prolog, 1996.

M. Steppler and M. Lott, SPEET ???SDL Performance Evaluation Tool, SDL'97, pp.53-67, 1997.
DOI : 10.1016/B978-044482816-3/50005-8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.6672

L. Sterling and E. Shapiro, The Art of Prolog, IEEE Expert, vol.2, issue.2, 1994.
DOI : 10.1109/MEX.1987.4307074

C. Lin, T. , and S. Pink, Mobicast: a multicast scheme for wireless networks, pp.259-271, 2000.

T. Clausen and P. Jacquet, Optimized Link State Routing Protocol (OLSR) - RFC3626. INRIA, ietf edition, 2003.

O. Tickoo and B. Sikdar, Queueing analysis and delay mitigation in IEEE 802.11 random access MAC based wireless networks, IEEE INFOCOM 2004, pp.7-11, 2004.
DOI : 10.1109/INFCOM.2004.1357025

S. Kishor and . Trivedi, Probability and Statistics with Reliability, Queuing, and Computer Science Applications, 2001.

A. Vahdat and D. Becker, Epidemic routing for partially-connected ad hoc networks, 2000.

H. Van and . Vliet, Sotware Engineering: Principles and Practice, 1999.

Y. Wang and M. Xiong, Monte Carlo Simulation of LEACH Protocol for Wireless Sensor Networks, Sixth International Conference on Parallel and Distributed Computing Applications and Technologies (PDCAT'05), pp.85-88, 2005.
DOI : 10.1109/PDCAT.2005.168

T. Watteyne, I. Auge-blum, and S. Ubeda, Formal qos validation approach on a real-time mac protocol for wireless sensor networks, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070239

M. Wei, F. Dubois, D. Vincent, and P. Combes, Looking for better integration of design and performance engineering, SDL 2003 : System design, pp.1-17, 2003.

O. Wibling, Ad hoc routing protocol validation, 2005.

. Wsim, WSim simulator, worldsens.citi.insa-lyon.fr/joomla/index.php. [147] WSNet. Wireless Sensor Network simulator

N. Xu, S. Rangwala, K. Chintalapudi, D. Ganesan, A. Broad et al., A wireless sensor network For structural monitoring, Proceedings of the 2nd international conference on Embedded networked sensor systems , SenSys '04, pp.13-24, 2004.
DOI : 10.1145/1031495.1031498

F. Zaïdi, A. Cavalli, and E. Bayse, NetworkProtocol Interoperability Testing based on Contextual, 24th Annual ACM Symposium on Applied Computing, pp.321-327, 2009.

I. Zakkuidin, T. Hawkins, and N. Moffat, Towards A Game Theoretic Understanding of Ad-Hoc Routing, Electronic Notes in Theoretical Computer Science, vol.119, issue.1, pp.67-92, 2005.
DOI : 10.1016/j.entcs.2004.07.009

.. Verification, 18 5.2.1 Model checking approaches, p.22