Model-based re-engineering of control application : Code generation and verification