. La-conversion-d-'un-appel-d, opération dans le contexte d'´ evaluation nécessite un processus plus complexe. Dans ce contexte, le langage OCL4MBT ajoute la restriction qu'un appel d'opération ne doit pas modifier l'´ etat du système. Le processus de conversion d

. Déterminer, appel est valide en contrôlant que la pré-condition de l'opération appelée est vérifiée avec les valeurs passées en paramètre. Par conséquent, cette condition est ajoutée dans le précédent contexte d'´ evaluation du code OCL4MBT. En pratique, ce contexte est rencontré dans la condition de l'opérateur " if then else

?. , |. , |. , ?. Ops, and ?. Var, v n } ? smt |= svar anim (x : Event) | x , svar anim (trig x : Bool ), svar anim (step x : Bool ) ? F

D. Choix-d-'une-stratégie, après les mesures présentées par le tableau 11.2, le critère principal de sélection d'une stratégie sans l'utilisation de la parallélisation est la taille et la complexité du modèle. Le modèle eCinema correspondàcorrespond`correspondà une taille pivot. En dessous, les meilleures stratégies en terme de temps de génération sont par ordre décroissant : Path, Step-Increase, Space-Search :breadth et Space-Search :depth

. Quand-la-taille, les performances des stratégies Space- Search :breadth et Step-Increase se dégradent. A contrario, les stratégies Space- Search :depth et Path ont de meilleurs résultats. La seule constante vérifiée sur l'ensemble des modèles est que la stratégie Basic a systématiquement les temps de génération les plusélevésplusélevés

S. La-stratégie, Increase collaboratif a des temps inférieurs de 10 % en moyennè a ceux de la stratégie Step-Increase sur l'ensemble des modèles. Par contre, la stratégie Space-Search collaboratif a des temps supérieurssupérieurs`supérieursà la stratégie Space-Search :depth

. Le-diagramme-d-'´-etats-transitions-qui-est-optionnel,-renseigne-sur-le-comportement-du-modèle, Ainsi l'´ evolution du système est précisée aux travers des opérations des classes et des transitions du diagramme d'´ etats-transitions. La caractéristique principale de ce langage est de définir un nombre fini d'´ etats du système Pour représenter le modèle et sonévolutionsonévolution, notre démarche le considère comme un système de transitions o` u l'´ etat initial est défini par le diagramme d'objets et les transitions correspondent aux opérations du diagramme de classes et/ou aux transitions du diagramme d'´ etats-transitions. Ainsi un test est une séquence de transitions 13.1. Au niveau du modèle 13.1.2 Aidè a l'´ ecriture du modèle Notre démarche, de part l'utilisation d'un langage de modélisation dédié aux tests, se situe clairement dans la catégorie du testàtest`testà partir de modèles o` u ces derniers sont utilisés uniquement pour la génération de tests. Par conséquent, rien ne s'opposèopposè a optimiser ces derniers pour améliorer les performances de notre méthode. Il est ainsi envisageable de fournir une analyse préliminaire du modèle afin de guider l'ingénieur de test lors des choix de modélisations, exemple de choix est fourni lors de la modélisation du Robot. Lapremì ere possibilité est de modéliser les différentspì eces par uné enumération. La présence d'unepì ece sur un tapis roulant ou dans le bras du robot est ainsi encodée par un attribut. L'absence depì ece est modélisée par une valeur spéciale dans l'´ enumération

J. Abrial, J. Abrial, and A. Hoare, The Bbook : assigning programs to meanings, 2005.

[. Anastasakis, B. Bordbar, G. Georg, and I. Ray, UML2Alloy: A Challenging Model Transformation, Model Driven Engineering Languages and Systems, pp.436-450, 2007.
DOI : 10.1007/978-3-540-75209-7_30

R. Krzysztof, M. Apt, and . Wallace, Constraint logic programming using ECLiPSe, 2006.

[. Bolognesi and E. Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, vol.14, issue.1, pp.25-59, 1987.
DOI : 10.1016/0169-7552(87)90085-7

R. Brummayer and A. Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, Tools and Algorithms for the Construction and Analysis of Systems, pp.174-177, 2009.
DOI : 10.1007/978-3-540-78800-3_24

D. [. Berardi, G. Calvanese, and . Giacomo, Reasoning on UML class diagrams, Artificial Intelligence, vol.168, issue.1-2, pp.70-118, 2005.
DOI : 10.1016/j.artint.2005.05.003
URL : http://doi.org/10.1016/j.artint.2005.05.003

[. Bouquet, S. Debricon, B. Legeard, and J. Nicolet, Extending the unified process with model-based testing, MoDeVa'06, 3rd Int. Workshop on Model Development, Validation and Verification, pp.2-15, 2006.
URL : https://hal.archives-ouvertes.fr/hal-01222822

[. Barrett, M. Deters, A. Oliveras, and A. Stump, Design and results of the 4th annual satisfiability modulo theories competition (smt-comp, 2008.

A. Belinfante, JTorX: A Tool for On-Line Model-Driven Test Derivation and Execution, Tools and Algorithms for the Construction and Analysis of Systems, pp.266-270, 2010.
DOI : 10.1007/978-3-642-12002-2_21

[. Brandes, M. Eiglsperger, J. Lerner, and C. Pich, Graph markup language (graphml) Handbook of Graph Drawing and Visualization (Discrete Mathematics and Its Applications), 2010.

A. Belinfante, L. Frantzen, and C. Schallhart, 14 Tools for Test Case Generation, Model-Based Testing of Reactive Systems, pp.391-438, 2005.
DOI : 10.1007/11498490_18

F. Bouquet, C. Grandpierre, and B. Legeard, Fabien Peureux, Nicolas Vacelet, and Mark Utting. A subset of precise uml for model-based testing, Proceedings of the 3rd international workshop on Advances in model-based testing, pp.95-104, 2007.

[. Bozga, S. Graf, and L. Mounier, IF-2.0: A Validation Environment for Component-Based Real-Time Systems, Proceedings of Conference on Computer Aided Verification, CAV'02, pp.343-348, 2002.
DOI : 10.1007/3-540-45657-0_26
URL : https://hal.archives-ouvertes.fr/hal-00357518

W. Barnett, L. Grieskamp, W. Nachmanson, and . Schulte, Nikolai Tillmann, and Margus Veanes. Model-based testing with asml .net, 1st European Conference on Model-Driven Software Engineering, pp.12-19, 2003.

[. Boussemart, F. Hemery, and C. Lecoutre, De ac3à ac3`ac3à ac7, Technique et Science Informatiques, vol.22, issue.1, pp.267-280, 2003.

D. Achim, . Brucker, P. Matthias, D. Krieger, B. Longuet et al., A specification-based test case generation method for uml/ocl, Models in Software Engineering, pp.334-348, 2011.

B. [. Bouquet and . Legeard, Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study, Proceedings of the International Conference on Formal Methods Europe (FME'03), volume 2805 of LNCS, pp.778-795, 2003.
DOI : 10.1007/978-3-540-45236-2_42

[. Bouquet, B. Legeard, and F. Peureux, CLPS-B???A Constraint Solver for B, Tools and Algorithms for the Construction and Analysis of Systems, pp.188-204, 2002.
DOI : 10.1007/3-540-46002-0_14

[. Barnett, K. Rustan, M. Leino, and W. Schulte, The spec# programming system : An overview. In Construction and analysis of safe, secure, and interoperable smart devices, pp.49-69, 2005.

[. Barrett, A. Stump, and C. Tinelli, The smt-lib standard : Version 2.0, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, 2010.

J. Bofill, M. Suy, and . Villaret, A System for Solving Constraint Satisfaction Problems with SMT, Theory and Applications of Satisfiability Testing?SAT 2010, pp.300-305, 2010.
DOI : 10.1007/978-3-642-14186-7_25

M. Buchi and W. Weck, A plea for grey-box components, Turku Centre for Computer Science, 1997.

. Achimd, B. Brucker, and . Wolff, Hol-ocl : A formal proof environment for uml/ocl, Fundamental Approaches to Software Engineering, pp.97-100, 2008.

D. Achim, B. Brucker, and . Wolff, hol-testgen, Fundamental Approaches to Software Engineering, pp.417-420, 2009.

J. Cabot, R. Clarisó, and D. Riera, UMLtoCSP, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering , ASE '07, pp.547-548, 2007.
DOI : 10.1145/1321631.1321737

J. Cabot, R. Clarisó, and D. Riera, Verifying UML/OCL Operation Contracts, Integrated Formal Methods, pp.40-55, 2009.
DOI : 10.1145/299917.299919

D. M. Cohen, S. R. Dalal, M. L. Fredman, and G. C. Patton, The aetg system : An approach to testing based on combinatorial design. Software Engineering, IEEE Transactions on, vol.23, issue.7, pp.437-444, 1997.

[. Cytron and J. Ferrante, An efficient method of computing static single assignment form, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, 1989.
DOI : 10.1145/75277.75280

[. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani, The MathSAT5 SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, pp.93-107, 2013.
DOI : 10.1007/978-3-642-36742-7_7

[. Clarke, T. Jéron, V. Rusu, and E. Zinovieva, STG: A Symbolic Test Generation Tool, Tools and Algorithms for the Construction and Analysis of Systems, pp.470-475, 2002.
DOI : 10.1007/3-540-46002-0_34

[. Dutertre and L. D. Moura, The yices smt solver, 2006.

[. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

[. Moura and N. Bjørner, Z3: An Efficient SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

[. Fourneret and F. Bouquet, Impact analysis for uml/ocl statechart diagrams based on dependence algorithms for evolving critical software. Laboratoire d'Informatique de Franche-Comté, pp.2010-2016, 2010.

[. Fernandez, ALDEBARAN : un systeme de vérification par réduction de processus communicants, 1988.

G. Fraser and A. Gargantini, An Evaluation of Model Checkers for Specification Based Test Case Generation, 2009 International Conference on Software Testing Verification and Validation, pp.41-50, 2009.
DOI : 10.1109/ICST.2009.33

P. Farail, G. Pierre, A. Canals, C. L. Camus, D. Sciamma et al., The topcased project : a toolkit in open source for critical aeronautic systems design, pp.54-59, 2006.

. Jean-claude, H. Fernandez, A. Garavel, L. Kerbrat, R. Mounier et al., Cadp a protocol validation and verification toolbox, Computer Aided Verification, pp.437-440, 1996.

[. Gogolla, F. Büttner, and M. Richters, USE: A UML-based specification environment for validating UML and OCL, Science of Computer Programming, vol.69, issue.1-3, pp.27-34, 2007.
DOI : 10.1016/j.scico.2007.01.013

J. Grabowski, D. Hogrefe, G. Réthy, I. Schieferdecker, A. Wiles et al., An introduction to the testing and test control notation (TTCN-3), Computer Networks, vol.42, issue.3, pp.375-403, 2003.
DOI : 10.1016/S1389-1286(03)00249-4

J. Michael, . Gordon, F. Tom, and . Melham, Introduction to HOL : a theorem proving environment for higher order logic [GP95] JanFriso Groote and Alban Ponse. The syntax and semantics of µcrl, Algebra of Communicating Processes, Workshops in Computing, pp.26-62, 1993.

Y. Joseph, P. Halpern-halbwachs, P. Caspi, D. Raymond, ]. A. Pilaudhft00 et al., The synchronous data flow programming language lustre Formal test automation : The conference protocol with phact Alain Le Guennec, and François Pennaneac'h . Umlaut : an extendible uml transformation framework, Presburger arithmetic with unary predicates is pi 1 1 complete Proceedings of the IEEE Proceedings of the IFIP TC6/WG6.1 13th International Conference on Testing Communicating Systems : Tools and Techniques Conference Proceedings Automated Software Engineering 14th IEEE International Conference on, pp.56-21305, 1991.

A. Holmes and M. Kellogg, Automating Functional Tests Using Selenium, AGILE 2006 (AGILE'06), 2006.
DOI : 10.1109/AGILE.2006.19

A. Hartman and K. Nagin, The AGEDIS tools for model based testing, ACM SIGSOFT Software Engineering Notes, vol.29, issue.4, pp.129-132, 2004.
DOI : 10.1145/1013886.1007529

J. Hartmann, M. Vieira, H. Foster, and A. Ruder, Umlbased test generation and execution, pp.2012-2017, 2004.

D. Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology, vol.11, issue.2, pp.256-290167, 2002.
DOI : 10.1145/505145.505149

C. Jard and T. Jéron, TGV: theory, principles and algorithms, International Journal on Software Tools for Technology Transfer, vol.17, issue.4, pp.297-315, 2005.
DOI : 10.1007/s10009-004-0153-x
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.4262

. Bibliographie, +. Kfdb, H. Kyas, . Fecher, S. Frank et al., Jozef Hooman , Mark Van Der Zwaag, Tamarah Arons, and Hillel Kugler. Formalizing uml models and ocl constraints in pvs, Electronic Notes in Theoretical Computer Science, vol.115, pp.39-47, 2005.

[. Kuhlmann, L. Hamann, and M. Gogolla, Extensive Validation of OCL Models by Integrating SAT Solving into USE, Objects, Models, Components, Patterns, pp.290-306, 2011.
DOI : 10.1007/978-3-642-21952-8_21

[. Kwast, . Wilts, J. Kloosterman, and . Kroon, User manual of the conformance kit, Dutch PTT Research, 1991.

T. Gary, . Leavens, L. Albert, C. Baker, and . Ruby, Jml : a java modeling language, Formal Underpinnings of Java Workshop. Citeseer, 1998.

[. Lann, An analysis of the Ariane 5 flight 501 failure-a system engineering perspective, Proceedings International Conference and Workshop on Engineering of Computer-Based Systems, pp.339-346, 1997.
DOI : 10.1109/ECBS.1997.581900

A. [. Lötzbeyer and . Pretschner, Autofocus on constraint logic programming, In IN PROC. (CONSTRAINT) LOGIC PROGRAM- MING AND SOFTWARE ENGINEERING, 2000.

[. Legeard, F. Peureux, and M. Utting, Automated Boundary Testing from Z and B, FME 2002 : Formal Methods?Getting IT Right, pp.21-40, 2002.
DOI : 10.1007/3-540-45614-7_2

B. Marre and A. Arnould, Test sequences generation from LUSTRE descriptions: GATEL, Proceedings ASE 2000. Fifteenth IEEE International Conference on Automated Software Engineering, pp.229-237, 2000.
DOI : 10.1109/ASE.2000.873667

R. Mugridge and W. Cunningham, Fit for developing software : framework for integrated tests, 2005.

N. Nethercote, J. Peter, R. Stuckey, S. Becket, . Brand et al., MiniZinc: Towards a Standard CP Modelling Language, Principles and Practice of Constraint Programming?CP 2007, pp.529-543, 2007.
DOI : 10.1007/978-3-540-74970-7_38
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.132.9321

A. Pretschner, W. Prenninger, S. Wagner, C. Kühnel, M. Baumgartner et al., One evaluation of model-based testing and its automation, Proceedings of the 27th international conference on Software engineering, pp.392-401, 2005.

J. Stacy and . Prowell, Tml : A description language for markov chain usage models. Information and Software Technology, pp.835-844, 2000.

J. Stacy and . Prowell, Jumbl : A tool for model-based statistical testing, System Sciences Proceedings of the 36th Annual Hawaii International Conference on, 2003.

M. Richters and M. Gogolla, On Formalizing the UML Object Constraint Language OCL, Conceptual Modeling?ER'98, pp.449-464, 1998.
DOI : 10.1007/978-3-540-49524-6_35

[. Rumbaugh, I. Jacobson, and G. Booch, Unified Modeling Language Reference Manual, The. Pearson Higher Education, 2004.

R. Rosenfeld, Two decades of statistical language modeling: where do we go from here?, Proceedings of the IEEE, vol.88, issue.8, pp.1270-1278, 2000.
DOI : 10.1109/5.880083

J. Peter, R. Stuckey, J. Becket, and . Fischer, Philosophy of the minizinc challenge, Constraints, vol.15, issue.3, pp.307-316, 2010.

D. Steinberg, F. Budinsky, E. Merks, and M. Paternostro, EMF : eclipse modeling framework, 2008.

]. M. Seg-+-96, A. Schmitt, J. Ek, D. Grabowski, B. Hogrefe et al., Autolink putting sdl-based test generation into practice, Testing of Communicating Systems, pp.227-243, 1996.

M. Shafique and Y. Labiche, A systematic review of model based testing tool support, p.21, 2010.

[. Schulte, G. Lagerkvist, . Tack, and . Gecode, Software download and online material at the website, 2006.

[. Shankar, S. Owre, M. John, D. Rushby, and . Stringer-calvert, Pvs prover guide, pp.11-12, 2001.

S. Spitz, F. Slomka, and M. Dörfel, Sdl* -an annotated specification language for engineering multimedia communication systems, 6th Open Workshop On High Speed Networks, Institut für Bibliographie Nachrichtenvermittlung und Datenverarbeitung, 1997.

[. Soeken, R. Wille, and R. Drechsler, Verifying dynamic aspects of UML models, 2011 Design, Automation & Test in Europe, pp.1-6, 2011.
DOI : 10.1109/DATE.2011.5763177

R. Mathias-soeken, M. Wille, M. Kuhlmann, R. Gogolla, and . Drechsler, Verifying uml/ocl models using boolean satisfiability, Proceedings of the Conference on Design, Automation and Test in Europe European Design and Automation Association, pp.1341-1344, 2010.

[. Tassey, The economic impacts of inadequate infrastructure for software testing. National Institute of Standards and Technology, pp.2-3, 2002.

J. Tretmans and E. Brinksma, Torx : Automated model-based testing, 2003.

N. Tillmann and J. D. Halleux, Pex???White Box Test Generation for .NET, Tests and Proofs, pp.134-153, 2008.
DOI : 10.1007/978-3-540-79124-9_10

[. Torlak and D. Jackson, Kodkod: A Relational Model Finder, Tools and Algorithms for the Construction and Analysis of Systems, pp.632-647, 2007.
DOI : 10.1007/978-3-540-71209-1_49

J. Tretmans, Model Based Testing with Labelled Transition Systems, Formal methods and testing, pp.1-38, 2008.
DOI : 10.1007/978-3-540-78917-8_1

M. Utting and B. Legeard, Practical model-based testing : a tools approach, 2010.

[. Utting, A. Pretschner, and B. Legeard, A taxonomy of model-based testing approaches. Software Testing, Verification and Reliability, pp.297-312, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00940611

. Vaandrager, Does it pay off ? model-based verification and validation of embedded systems, pp.43-66, 2006.

. Vcg-+-08-]-margus, C. Veanes, W. Campbell, W. Grieskamp, N. Schulte et al., Model-based testing of object-oriented reactive systems with spec explorer, Formal methods and testing, pp.39-76, 2008.

[. Weißleder, Parteg (partition test generator) See http ://parteg . sourceforge. net, 2009.

A. Stephen, D. White, and . Miers, BPMN modeling and reference guide : understanding and using BPMN, Future Strategies Inc, 2008.