Towards Verifying Model Compilers

International audienceIn this paper we propose a methodological and technical approach to develop model compilers which provide formal proof of semantic preservation and complement model-level verification activities with formal analysis on the generated source code. Our paper also details which characteristic a programming language shall exhibit to be used as target of a model compiler. Finally, we evaluate the impact of using formal programming languages on the development and qualification of model compilers