B. Akshay, P. Bollig, M. Gastin, K. Mukund, and . Narayan-kumar, Distributed timed automata with independently evolving clocks, CONCUR 2008-Concurrency Theory, pp.82-97, 2008.
DOI : 10.1007/978-3-540-85361-9_10
URL : https://hal.archives-ouvertes.fr/hal-01089524

M. Abadi and L. Cardelli, A Theory of Objects, 1996.

R. Alur and D. L. Dill, A theory of timed automata. Theoretical Computer Science, vol.126, pp.183-235, 1994.

C. André, Syntax and Semantics of the Clock Constraint Specification Language (CCSL), INRIA, 2009.

B. Bcc-+-08]-albert-benveniste, L. Caillaud, P. Carloni, A. Caspi, and . Sangiovanni-vincentelli, Composing Heterogeneous Reactive Systems, ACM Transactions on Embedded Computing Systems (TECS), vol.7, issue.4, 2008.

G. Berry, The foundations of Esterel, Gordon Plotkin, Colin Stirling, and Mads Tofte, pp.425-454, 2000.

G. Berry, Scade: Synchronous design and validation of embedded control software, Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, pp.19-33, 2007.

F. Boulanger, C. Hardebolle, C. Jacquet, and D. Marcadet, Semantic adaptation for models of computation, Eleventh International Conference on Application of Concurrency to System Design, pp.153-162, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00605273

F. Boulanger, C. Jacquet, C. Hardebolle, and I. Prodan, TESL: a language for reconciling heterogeneous 99 bibliography execution traces, Twelfth ACM/IEEE International Conference on, pp.114-123, 2014.

D. Achim, B. Brucker, and . Wolff, Monadic sequence testing and explicit test-refinements, Tests and Proofs-10th International Conference, TAP 2016, Held as Part of STAF 2016, pp.17-36, 2016.

. Benoit-combemale, H. C. Betty, R. B. Cheng, J. France, B. Jezequel et al., Globalizing Domain-Specific Languages, LNCS, Programming and Software Engineering, vol.9400, 2015.

A. Church, A set of postulates for the foundation of logic, Annals of Mathematics, vol.33, issue.2, pp.346-366, 1932.

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.5, issue.2, pp.56-68, 1940.

J. Deantoni, C. André, and R. Gascon, CCSL denotational semantics, Inria, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01082274

T. A. Luca-de-alfaro and . Henzinger, Interface automata, SIGSOFT Softw. Eng. Notes, vol.26, issue.5, pp.109-120, 2001.

D. Dalen, . Logic, . Structure, ;. Universitext, J. W. Eker et al., Taming heterogeneity-the Ptolemy approach, Proceedings of the IEEE, vol.91, issue.1, pp.127-144, 1979.

P. L. Guernic, A. Benveniste, P. Bournai, and T. Gautier, Synchronous data flow programming with the language SIGNAL, 2nd IFAC Workshop on Adaptive Systems in Control and Signal Processing, vol.20, pp.359-364, 1986.

M. Garnacho, J. Bodeveix, and M. Filaliamine, A mechanized semantic framework for real-time systems, Formal Modeling and Analysis of Timed Systems: 11th International Conference, FORMATS 2013, pp.106-120, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01231769

F. Haftmann, Haskell-style type classes with Isabelle/Isar, 2013.

C. Hardebolle and F. Boulanger, Multi-formalism modelling and model execution, Special Issue on the International Summer School on Software Engineering, vol.31, pp.193-203, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00421169

R. Hale, R. Cardell-oliver, and J. Herbert, An embedding of timed transition systems in HOL, Formal Methods in System Design, vol.3, issue.1, pp.151-174, 1993.

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language Lustre, Proceedings of the IEEE, vol.79, issue.9, pp.1305-1320, 1991.

J. E. Hopcroft, R. Motwani, and J. D. Ullman, troduction to automata theory, languages, and computation, vol.32, pp.60-65, 2001.

D. Jung and P. Tsiotras, Modeling and hardwarein-the-loop simulation for a small unmanned aerial vehicle, AIAA Infotech@ Aerospace 2007 Conference and Exhibit, p.2768, 2007.

G. Kahn, The semantics of simple language for parallel programming, IFIP Congress, pp.471-475, 1974.

A. Ku?era and J. Strej?ek, The stuttering principle revisited, Acta Informatica, vol.41, issue.7-8, pp.415-434, 2005.

M. Krichen and S. Tripakis, Conformance testing for realtime systems, Form. Methods Syst. Des, vol.34, issue.3, pp.238-304, 2009.

L. Lamport, What good is temporal logic, Congress on Information Processing, pp.657-668, 1983.

P. Le-guernic, T. Gautier, J. Talpin, and L. Besnard, Polychronous automata, TASE 2015, 9th International Symposium on Theoretical Aspects of Software Engineering, pp.95-102, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01240440

C. Livadas, J. Lygeros, and N. A. Lynch, High-level modeling and analysis of the traffic alert and collision avoidance system (tcas), Proceedings of the IEEE, vol.88, issue.7, pp.926-948, 2000.

E. A. Lee and D. G. Messerschmitt, Synchronous data flow. Proceedings of the IEEE, vol.75, pp.1235-1245, 1987.

A. Edward, A. L. Lee, and . Sangiovanni-vincentelli, The tagged signal model a preliminary version of a denotational framework for comparing models of computation. Technical Report UCB/ERL M96/33, 1996.

N. G. Leveson and C. S. Turner, An investigation of the Therac-25 accidents, Computer, vol.26, issue.7, pp.18-41, 1993.

F. Mallet, Clock constraint specification language: specifying clock constraints with UML/Marte, Innovations in Systems and Software Engineering, vol.4, issue.3, pp.309-314, 2008.

F. Mallet, J. Deantoni, C. André, and R. Simone, The Clock Constraint Specification Language for building timed causality models, Innovations in Systems and Software Engineering, vol.6, issue.1-2, pp.99-106, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00464894

D. Matichuk, T. Murray, and M. Wenzel, Eisbach: A proof method language for Isabelle, Journal of Automated Reasoning, vol.56, issue.3, pp.261-282, 2016.

P. J. Mosterman, J. Sztipanovits, and S. Engell, Computerautomated multiparadigm modeling in control systems technology, IEEE Transactions on Control Systems Technology, vol.12, issue.2, pp.223-234, 2004.

L. Muliadi, Discrete event modeling in ptolemy ii. Technical Report UCB/ERL M99/29, EECS Department, 1999.

J. Pieter, H. Mosterman, and . Vangheluwe, Computer automated multi-paradigm modeling: An introduction, SIMULATION, vol.80, issue.9, pp.433-450, 2004.

H. Van, T. Balabonski, F. Boulanger, C. Keller, B. Valiron et al., A symbolic operational semantics for TESL-with an application to heterogeneous system testing, Formal Modeling and Analysis of Timed Systems-15th International Conference, pp.318-334, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01583815

T. Nipkow, Structured proofs in Isar/HOL, Types for Proofs and Programs, pp.259-278, 2003.

T. Nipkow and G. Klein, Concrete Semantics: With Isabelle/HOL, 2014.

T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: A Proof Assistant for Higher-order Logic, 2002.

M. and J. Deantoni, Scheduling Multi Clock Real Time Systems: From Requirements to Implementation, International Symposium on Object/Component/Serviceoriented Real-time Distributed Computing, number 14th in IEEE international Symposium on Object/Component/service Oriented Real-Time Distributed Computing, vol.57, p.50, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00586851

C. Paulin-mohring, Modelisation of timed automata in Coq, Theoretical Aspects of Computer Software: 4th International Symposium, TACS 2001 Sendai, pp.298-315, 2001.

, System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org, 2014.

B. Selic and S. Gerard, Modeling and Analysis of Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems. The MK/OMG Press, 2013.

J. E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, 1977.

J. Tbg-+-13]-jean-pierre-talpin, M. Brandt, K. Gemünde, S. Schneider, and . Shukla, Constructive polychronous systems, Logical Foundations of Computer Science, vol.7734, 2013.

J. Tretmans, Test generation with inputs, outputs and repetitive quiescence. Software-Concepts and Tools, vol.17, pp.103-120, 1996.

M. Ezequiel-vara-larsen, J. Deantoni, B. Combemale, and F. Mallet, A behavioral coordination operator language (BCOoL), 18th International Conference on Model Driven Engineering Languages and Systems, 2015.

S. Weeks, Whole-program Compilation in MLton, Proceedings of the 2006 Workshop on ML, ML '06, pp.1-1, 2006.

J. B. Wells, Typability and type checking in System F are equivalent and undecidable, Annals of Pure and Applied Logic, vol.98, issue.1, pp.111-156, 1999.

G. Winskel, The Formal Semantics of Programming Languages: An Introduction, 1993.

M. Zhang and F. Mallet, An executable semantics of Clock Constraint Specification Language and its applications, Formal Techniques for Safety-Critical Systems: 4th International Workshop, FTSCS 2015, pp.37-51, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01353824

, Proof sketch of irrationality of ? 2 in Isabelle/HOL, p.33

, Listing 2 Specification of a clock watch in TESL?, p.36

, Listing 3 Specification of a radiotherapy machine in TESL?, p.41

, Listing 4 Specification of a power window in TESL?, p.43

, Listing 5 Specification of an airplane takeoff in TESL, p.58

. , Listing 6 Specification of concurrent computations for two CPUs in TESL, vol.87

. , Definition (Timed Automaton [AD94a])

. .. , Definition (Grammar of the untyped ?-calculus), p.23

. .. , Definition (Reductions of the untyped ?-calculus), p.23

. .. , Definition (Equivalence in the untyped ?-calculus), p.23

. , Definition (Typing Rules of ? ? )

. .. , Definition (Grammar of ML-style), p.27

. .. , Definition (Type schemes in ML-style), p.27

. , Definition (Deduction System)

. , Definition (Rules of Natural Deduction)

. .. , Definition (Projections for Ticks and Tags), p.37

. , Grammar of TESL?)

. .. , Definition (Interpretation of TESL? formulae), vol.46

. , Definition (Tag Variables)

. , Definition (Introduction Rule ? i )

. , Grammar of TESL )

. .. , Definition (Interpretation of TESL formulae), p.61

. .. , Definition (Extended Run Primitives for TESL ), p.62

. .. , Extended Elimination Rules ? e for TESL ), vol.63

. , Grammar of TESL)

. .. , Extended Elimination Rules ? e for TESL), p.70

. .. , Definition (Stepwise Interpretation of TESL formulae), p.76

. .. , Definition (Interpretation of Configurations), p.79

. .. , Theorem (Fixpoint in a CPO (Tarski, Kleene)), p.22

. .. , Theorem (Confluence of ?-calculus (Church, Rosser)), p.23

. Lemma-(associativity, . Commutativity, . Idempotence, and ). .. Neutrality,

;. .. Lemma, Decidability of Run Contexts), p.48

. Lemma,

. Lemma-(stepwise-associativity, . Commutativity, . Idempotence, and ). .. Neutrality,

. Lemma, Start Configuration)

. Lemma, Sound Reduction)

). .. Theorem-;-soundness,

. Lemma, Complete Direct Successors)

). .. Theorem-;-completeness,

. Lemma, Instant Index Increase)

). .. Theorem-;-progress,