Towards Reliable LLM-Based Model Driven Engineering: when Full Syntax Checking and Formal Verification Join the Loop

Model-Driven Engineering facilitates the design of embedded systems by promoting abstraction and enabling early verification of design correctness. Recent approaches have integrated Large Language Models into MDE workflows to automatically generate models from textual specifications. However, these models often require extensive prompt refinement and lack formal guarantees of correctness. This paper introduces an enhanced LLM-based generation process in TTool-AI, incorporating a novel dual feedback loop that combines automated syntactic checking with formal verification of safety properties. The loop iteratively refines LLM-generated SysML block and state-machine diagrams to ensure syntactic validity and verify safety properties. First experimental evaluation on both academic and industrial-grade specifications demonstrates that the proposed mechanism reliably produces syntactically correct models, enabling direct model checking of LLM-produced models and reducing the effort required by engineers to obtain correct-by-construction designs.