Realizability of embedded controllers: from hybrid models to correct implementations