The importance of the language semantics for code generation and frameworks for code generation in model-driven development

Question

I am implementing worflow where the code in industrial programming languages (JavaScript and Java) should be generated from the formal (formally verified) expressions (from ontologies as objects and rule formulas as behaviors). What is the best pratice for such code generation? Are some frameworks available for this?

In my opinion the semantics of the programming language is required. And I should be able to do the code generation in two steps: 1) translate my formal epxressions into semantic expressions of the target language; 2) translate semantic expressions into executable code. In reality I can not find any work that connects semantics of programming language with the code generation.

Is there special kind of semantics of programming languages that is usable not only for the analysis of the programs but also for the generation of the programs?

My guess is that it should be really useful approach for generating formally verified code but I can not find research work about this. Are there trends of better keywords avilable for this?

Maybe - more relevant question is - what kind of compilers/translators the Model Driven Development tools use for the generation of source code (platform dependent code) and how semantics of programming language can be used for the construction of such compilers?

Note added. There already is complete unifying (denotational and operational) semantics of Java, JavaScript and other industrial programmin languages in the K framework. So - this is more question about application of K framework for code generation is that is possible at all?