The talk is a short description of main features of a portable simulator-verificator for reactive timed Abstract State Machines. The time may be continuous or discrete, the time constraints are linear (extendable to polynomial ones), the reaction may be instantaneous or with non deterministic bounded delays. The construction of runs goes on together with  the verification of a formula in a First Order Times Logic. There are simple languages for the generation of inputs, for resolving non determinism and for displaying of the results.