M. Autili, P. Inverardi, and P. Pelliccione, Graphical Scenarios for Specifying Temporal Properties: an Automated Approach, Automated Software Engineering, vol.14, issue.3, pp.293-340, 2007.

M. Valentin-besnard, P. Brun, F. Dhaussy, D. Jouault, C. Olivier et al., Towards one Model Interpreter for Both Design and Deployment, 3rd International Workshop on Executable Modeling (EXE), 2017.

M. Valentin-besnard, F. Brun, C. Jouault, P. Teodorov, and . Dhaussy, Embedded UML Model Execution to Bridge the Gap Between Design and Runtime, MDE@DeRun 2018 : First International Workshop on Model-Driven Engineering for Design-Runtime Interaction in Complex Systems, 2018.

M. Valentin-besnard, F. Brun, C. Jouault, P. Teodorov, and . Dhaussy, Unified LTL Verification and Embedded Execution of UML Models, ACM/IEEE 21th International Conference on Model Driven Engineering Languages and Systems (MODELS '18), 2018.

A. Bauer, M. Leucker, and C. Schallhart, Runtime Verification for LTL and TLTL, ACM Transactions on Software Engineering and Methodology, vol.20, issue.4, 2011.

T. Bochot, P. Virelizier, H. Waeselynck, and V. Wiels, Model Checking Flight Control Systems: The Airbus Experience, 31st International Conference on Software Engineering -Companion Volume, pp.18-27, 2009.

F. Ciccozzi, From Models to Code and Back : A Roundtrip Approach for Model-driven Engineering of Embedded Systems, 2014.

A. Duret, -. Lutz, and D. Poitrenaud, SPOT: An Extensible Model Checking Library Using Transition-Based Generalized Büchi Automata, Proceedings of the IEEE Computer Society's 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, MASCOTS '04, pp.76-83, 2004.

P. Dhaussy, L. Le-roux, and C. Teodorov, Vérification formelle de propriétés : Application de l'outil OBP au cas d'étude CCS, Génie logiciel, vol.109, 2014.

S. Gnesi and F. Mazzanti, A Model Checking Verification Environment for UML Statecharts, Proceedings of XLIII Congresso, 2005.

N. Halbwachs, F. Lagnier, and P. Raymond, Synchronous Observers and the Verification of Reactive Systems, Algebraic Methodology and Software Technology (AMAST'93), pp.83-96, 1994.

K. Havelund and G. Ro?u, Synthesizing Monitors for Safety Properties, Tools and Algorithms for the Construction and Analysis of Systems, pp.342-356, 2002.

K. Havelund and G. Ro?u, Efficient Monitoring of Safety Properties, International Journal on Software Tools for Technology Transfer, vol.6, issue.2, pp.158-173, 2004.

E. +-17]-padma-iyenghar, C. Pulvermueller, J. Westerkamp, M. Wuebbelmann, and . Uelschen, Model-Based Debugging of Embedded Software Systems, pp.107-132

A. Knapp, S. Merz, and C. Rauh, Model Checking Timed UML State Machines and Collaborations, Formal Techniques in Real-Time and Fault-Tolerant Systems, pp.395-414, 2002.

A. Knapp and J. Wuttke, Model Checking of UML 2.0 Interactions, Models in Software Engineering, pp.42-51, 2007.

L. Leroux, J. Delatour, and P. Dhaussy, Modélisation UML d'un régulateur de vitesse automobile, Génie logiciel, vol.109, 2014.

A. Mekki, M. Ghazel, and A. Toguyeni, Validating Time-constrained Systems Using UML Statecharts Patterns and Timed Automata Observers, Proceedings of the 3rd International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS'09, pp.112-124, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00801584

I. Ober, S. Graf, and I. Ober, Validation of UML Models via a Mapping to Communicating Extended Timed Automata, Model Checking Software, pp.127-145, 2004.

I. Ober, S. Graf, and I. Ober, Validating timed UML models by simulation and verification, International Journal on Software Tools for Technology Transfer, vol.8, issue.2, pp.128-145, 2006.

. Omg, Unified Modeling Language, 2017.

C. Teodorov, P. Dhaussy, and L. Roux, Environment-driven reachability for timed systems, International Journal on Software Tools for Technology Transfer, vol.19, issue.2, pp.229-245, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01373335

C. Teodorov, Z. Luka-le-roux, P. Drey, and . Dhaussy, Past-Free[ze] reachability analysis: reaching further with DAG-directed exhaustive state-space analysis. Software Testing, Verification and Reliability, vol.26, pp.516-542, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01373287