A. Group, Amma reference site

J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi, Uppaal -a tool suite for automatic verification of real-time systems, 4th DIMACS Workshop on Verification and Control of Hybrid Systems, pp.22-24, 1995.

L. Besnard, T. Gautier, and P. L. Guernic, Signal v4 -Inria version: Reference manual, 2005.

J. Bézivin, In search of a basic principle for model-driven engineering, Novatica Journal, issue.2, pp.21-24, 2004.

C. Brunette, Modeling Signal programs using the Generic Modeling Environment, 2005.

A. Gamatié and T. Gautier, Synchronous modeling of avionics applications using the signal language, The 9th IEEE Real-Time and Embedded Technology and Applications Symposium, 2003. Proceedings., 2003.
DOI : 10.1109/RTTAS.2003.1203046

A. Gamatié, T. Gautier, and L. Besnard, Modeling of Avionics Applications and Performance Evaluation Techniques Using the Synchronous Language SIGNAL, proceedings of Synchronous Languages, Applications, and Programming (SLAP'03). Portugal, 2003.
DOI : 10.1016/j.entcs.2003.05.002

N. Halbwachs, F. Lagnier, and C. , Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE, IEEE Transactions on Software Engineering, Special Issue on the Specification and Analysis of Real-Time Systems, 1992.
DOI : 10.1109/32.159839

N. Halbwachs, F. Lagnier, and P. Raymond, Synchronous Observers and the Verification of Reactive Systems, Algebraic Methodology and Software Technology, pp.83-96, 1993.
DOI : 10.1007/978-1-4471-3227-1_8

I. and V. University, The Gme user manual

I. and V. University, The Gme website

A. Kountouris and P. L. Guernic, Profiling of SIGNAL programs and its application in the timing evaluation of design implementations, IEE Colloquium on Hardware-Software Cosynthesis for Reconfigurable Systems, pp.6-7, 1996.
DOI : 10.1049/ic:19960225
URL : https://hal.archives-ouvertes.fr/hal-00544253

L. Guernic and T. Gautier, Data-flow to von Neumann: the signal approach In Advanced Topics in Data-Flow Computing, pp.413-438, 1991.

P. , L. Guernic, T. Gautier, M. L. Borgne, and C. L. Maire, Programming real-time applications with Signal, IEEE, pp.1321-1336, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075114

A. Ledeczi, M. Maroti, A. Bakay, G. Karsai, J. Garrett et al., The Generic Modeling Environment, Proc. of the IEEE Workshop on Intelligent Signal Processing (WISP'01), 2001.

F. Maraninchi and Y. Rémond, Mode-automata: About modes and states for reactive systems, proceedings of European Symposium On Programming, 1998.
DOI : 10.1007/BFb0053571

H. Marchand, P. Bournai, M. L. Borgne, and P. L. Guernic, Synthesis of discrete-event controllers based on the Signal environment, Discrete Event Dynamic System: Theory and Applications, pp.325-346, 2000.
URL : https://hal.archives-ouvertes.fr/hal-00546147

D. Mathaikutty, H. Patel, S. Shukla, and A. Jantsch, EWD, ACM Transactions on Design Automation of Electronic Systems, vol.12, issue.3, 2004.
DOI : 10.1145/1255456.1255470

T. Meyerowitz, J. Sprinkle, and A. Sangiovanni-vincentelli, A visual language for describing instruction sets and generating decoders, Proc. of the 4th ACM OOPSLA Workshop on Domain Specific Modeling, pp.23-32, 2004.

J. Sprinkle, J. Davis, and G. Nordstrom, A paradigm for teaching modeling environment design, Proc. of the OOPSLA'04 Educators Symposium (Poster Session), pp.24-28, 2004.

S. Yovine, KRONOS: a??verification tool for real-time systems, Software Tools for Technology Transfer, pp.123-133, 1997.
DOI : 10.1007/s100090050009

N. Returncode_type-_<process1, _<ProcessN name>_ret; end; % process PROCESS_CREATION % end; % process PARTITION_LEVEL_OS % process CREATE_RESOURCES = (? event initialize; ! integer resource1

R. , .. .. Processid_type-_<process1-name>_pid, and . Returncode_type-_<process1-name>_ret, _<ProcessN name>_PID, _<ProcessN name>_ret; real _<Process1 name>_dt, ..., _<ProcessN name>_dt; <Declarations of local ImaProcesses: <Process1 name>,...,<ProcessN name> > <Declaration of local signals and local types> end; %process <ImaPartition name>% B.4 IMA process Similarly to the ModuleLevelOS, the interpreter checks, for each IMA process, that the associated automaton is " well-formed, ProcessStatus_type status; integer Thus, there is one and only one initial transition and all INRIA