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

Bastien Sultan, Ludovic Apvrille

► To cite this version:

Bastien Sultan, Ludovic Apvrille. Towards Reliable LLM-Based Model Driven Engineering: when Full Syntax Checking and Formal Verification Join the Loop. 13th European Congress of Embedded Real Time Systems (ERTS), Feb 2026, Toulouse, France. 10.82331/ERTS.2026.52. hal-05513959

HAL Id: hal-05513959

https://hal.science/hal-05513959v1

Submitted on 16 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Towards Reliable LLM-Based Model Driven Engineering: when Full Syntax Checking and Formal Verification Join the Loop

Bastien Sultan<fnref n="1" />, Ludovic Apvrille<fnref n="1" />

¹ LTCI, Télécom Paris, Institut Polytechnique de Paris, Sophia-Antipolis, France
firstname.lastname@telecom-paris.fr

## ABSTRACT

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.

**Keywords:** Model-Driven Engineering – Large Language Models – Model Generation – Syntax Checking – Formal Verification

## 1. INTRODUCTION

Model-Driven Engineering (MDE) approaches are especially relevant to embedded systems design, where they facilitate abstraction and allow early verification of design correctness [1, 27]. Such verification is essential for demonstrating compliance with regulatory and certification constraints, particularly in the development of safety-critical embedded systems. In recent years, several contributions have explored the integration of Large Language Models (LLMs) into MDE processes to assist engineers [13], for example by generating models from textual specifications. However, LLMs often require time-consuming, iterative prompt refinement to produce responses that align with user expectations. This issue is well known to LLM users and has been, for instance, pointed out for UML model generation [6]. In addition, if these technologies offer significant potential for helping systems engineers and improving the quality of system architectures, they also feature inherent limitations such as bias and hallucinations, which make their direct use incompatible with the requirements of critical systems engineering. Consequently, solutions that enable the safe and trustworthy integration of AI into critical systems development are required to ensure compliance with sector-specific standards and best practices.

TTool-AI [3, 24, 25], an LLM-based assistant embedded in the MDE toolkit TTool<fnref n="1" />, represents a first step toward ad-

dressing this challenge. The tool supports engineers throughout various MDE stages, including generating SysML requirement diagrams from textual specification during analysis, or producing SysML block diagrams (BDs) and state-machine diagrams (SMDs) during design. To ensure high-quality outputs, TTool-AI drives the LLM using (1) domain-specific contextual knowledge and (2) an automated, incremental verification and feedback loop that iteratively refines the model until a minimal quality threshold is met. This mechanism has been shown to produce high-quality models within minutes [3], without requiring human intervention.

Nevertheless, the current feedback loop verifies a wide set of syntactic consistency rules but does not formally assess compliance with system requirements nor verifies the full syntactic correctness of the models. This paper introduces a new feedback loop aimed at improving the correctness of generated design models (i.e., a BD and its associated SMDs) with respect to syntax and to safety properties. Specifically, this AI-based loop integrates full syntactic verification and model checking [9, 21] into the model generation process: it triggers verification on the LLM-generated output, then automatically feeds back unmet safety properties to the LLM until the generated models satisfy them (or a limit is hit). At the current stage of our works, safety verification focuses on verifying state reachability in SMDs and the absence of deadlocks.

The rest of the paper is organized as follows. Section 2 reviews related work. Section 3 details our contribution within the TTool-AI generation process. Section 4 presents early experimental results. Finally, section 5 concludes and outlines future work.

## 2. RELATED WORK AND CONTEXT

Numerous studies have examined the adoption of MDE in embedded systems design. Akdur et al. [1] conducted such a survey, involving 627 engineers from 27 countries, and identified 14 previous studies on the topic, highlighting the interest of applying MDE to this context. This interest is further evidenced by the extensive body of literature on MDE methodologies and tools specifically tailored for embedded systems [22]. Among these, UML-based approaches are among the most widely adopted [1]. This is further supported by a substantial number of contributions (too many to cite exhaustively here) that propose UML/SysML-based engineering methodologies [11, 20, 23, 16] and domain-specific profiles [17, 18, 14], including MARTE [2] and AVATAR [19] (on which the paper focuses).

<footnote>Bastien Sultan et Ludovic Apvrille. This is an open-access article distributed under the terms of the Creative Commons Attribution 4.0 License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.</footnote>

<footnote n="1">¹https://ttool.telecom-paris.fr</footnote>
<figure><img src="image_2.png" /><figcaption>Figure 1. Design model LLM-based generation with the novel feedback loop. With respect to the previous loop [3, 24], steps **T4** and **T5** have been added, and **T3** has been enhanced.</figcaption></figure>

Among the top motivations for adopting MDE in embedded systems design are “cost savings, achieving shorter development time, reusability and quality improvement” [1]. Over the past three years, research has increasingly focused on further enhancing several of these aspects, mostly shorter development time, reusability and cost saving, through the integration of AI into MDE processes and tools. Di Rocco et al. [13] provide a comprehensive overview of the contributions to date on this topic. Their review highlights various strategies for integrating LLMs into MDE processes, including retrieval-augmented generation which consists in pruning LLMs with domain-specific contextual knowledge. TTool-AI [3, 24, 25] employs such a strategy alongside an automated feedback loop. In the context of generating SysML models from textual system specifications, this loop (1) algorithmically analyzes the models produced by the LLM and (2) iteratively refines the prompts until the output meets a predefined quality threshold in terms of consistency. Once this threshold is reached, the resulting model is automatically rendered graphically within TTool’s GUI. This feedback mechanism is a way to increase the correctness of LLM-generated models, providing engineers with a high-quality starting point for further development. This addresses a concrete engineering need, since a key motivation for the industrial adoption of MDE is the ability to obtain early feedback on the correctness of system designs [27]. Building on TTool-AI, the present paper aims to advance further this capability by adding a new feedback loop focusing on syntactic correctness and temporal logic property verification of generated state machines (one of the two most commonly used diagram types among embedded systems MDE practitioners [1]).

One way to verify the safety properties of a system is through model checking [9, 21]. This technique systematically explores the portion of the system's state space required to determine whether the predefined temporal-logic conditions (representing the safety properties) hold. It thus provides mathematically proven evidence of the model's (non-)compliance with the requirements. TTool includes a model-checker that

support verification of SysML models against safety and security properties [12], and a syntax checker. Our contribution integrates these checking capabilities into the TTool-AI feedback loop to iteratively improve the correctness of LLM-generated models. Other contributions on LLM/MDE integration have focused on ensuring sufficient output model quality. Most rely on expert analysis, for instance in the vibe modeling process [4], where modeling experts iteratively evaluate and refine the generated models. MITRE's SELMA modeling assistant [10] also relies on expert-based inspection and iterative refinement to ensure that LLM-produced models meet the desired quality threshold. Some approaches additionally incorporate algorithmic syntax verification [7], and several works have undertaken first steps toward the LLM-based generation of correct-by-construction models [15, 8]. However, to the best of our knowledge, no prior work has proposed a formal-verification-driven LLM-based model generation tool that integrates model-checking directly in the iterative feedback loop between the tool and the LLM.

### 3. INTEGRATING SAFETY VERIFICATION IN THE MODEL GENERATION LOOP

Figure 1 provides an overview of TTool-AI LLM-based design generation process [3, 24] now enriched with the contributions of the present paper (steps **T4** and **T5**, and an enhancement of **T3**). A design consists of a BD and a set of SMDs (one per block): the figure focuses on the SMD generation stage. More specifically, all tasks shown within the black dotted box in the figure are fully automated by the tool and require no user intervention. In detail, the process operates as follows.

**T1.** Based on the system specification (written in natural language, with no formal constraints) and the previously generated BD, TTool-AI constructs a prompt that integrates the specification, a textual representation of the BD, and specific knowledge about SMDs (including syntactic constraints and formatting requirements for the LLM's response). This prompt is then sliced into several sequential parts and sent to the LLM,
<figure><img src="image_3.png" /><figcaption>Figure 2. TTool interface displaying a generated SMD. Green backtracing shows that all states satisfy the safety properties.</figcaption></figure>

which produces a response (T2).

That response is then algorithmically analyzed (T3) by the tool against a set of constraints, checking the format of the response (i.e., whether it meets the required structure for parsing), the consistency of the generated SMDs, and (this point is a central contribution of the paper) their complete syntactic correctness. The rules checked to ensure syntactic correctness follow from the definitions of syntactic correctness given in [26], Section 3.1. They include, among others, verifying that attribute types are valid, that two connected signals have matching parameter types, that the underlying graphs of state-machine diagrams are connected, etc. The source code of the syntax checker used for this purpose is available on TTool's public Gitlab<fnref n="2" />. If errors are detected, a new prompt, incorporating both the identified issues and the previously generated SMDs, is constructed and sent back to the LLM, returning the process to T1.

If no error is found, the process advances to the safety properties verification loop. First, in step T4 the tool generates a set of safety properties for each SMD and verifies them using TTool's model checker [5]. This model checker operates directly on SysML semantics by building a state-space graph from the BD and SMDs and then exploring it to verify temporal logic properties. In the current implementation of the feedback loop, the generated properties enable to check whether: (1) every state in the SMD is reachable, and (2) the system is free from deadlocks. If any property is violated, a new prompt, containing the unsatisfied properties and the corresponding SMD, is sent to the LLM, returning the process once again to T1.

The process proceeds to step U1 either when all properties are satisfied or when the maximum number of iterations in the loop is reached. Indeed, since the LLM may fail to converge to a correct solution, and to minimize the cost of iterative querying, TTool-AI enables to set a cap on the maximum number of iterations. For this specific case, the paper introduces a novel

mechanism (T5) that archives each response produced during the loop and provides the user with the best generated model when no correct one is obtained within the allowed iterations. This mechanism relies on a scoring approach that accounts for both the proportion of the number *e* of remaining syntactic errors relative to the number *s* of checked syntactic rules, and the proportion of the number *u* of unsatisfied safety properties relative to the total number *p* of verified properties. More precisely, for each model, the score is computed as follows:

$$ Score(e, u, s, p) = \begin{cases} 100 \left(1 - \frac{e}{s}\right) & \text{if } e > 0 \land s > 0 \\ 100 + 100 \left(1 - \frac{u}{p}\right) & \text{if } e = 0 \land p > 0 \\ 100 & \text{if } e = 0 \land p = 0 \end{cases} $$

Once the best model is selected based on this score, the process advances to U1. At this point, the user reviews the proposed model. They may either validate the result (triggering stage T6, which generates the graphical SMDs within TTool's GUI), or, if unsatisfied with the model, provide feedback via TTool-AI's dialogue window, which redirects the process back to T1. This dual automatic feedback loop drives the LLM to converge toward responses that are increasingly accurate.

## 4. FIRST EXPERIMENTAL INSIGHTS

We evaluated design (i.e., a SysML BD and its set of SMDs) generation using the new loop presented in previous section. Evaluation concerns three system specifications: two toy specifications commonly used in Master's-level systems engineering courses, and a real-world specification of a dynamic positioning system (an embedded system that maintains a vessel's heading and position at sea based on a given setpoint). The specifications and generated models are available on a public GitHub repository<fnref n="3" />. Table 1 summarizes the results, showing the number of triggered safety verification loops, token and monetary cost, required time, and the number of remaining syntactic and semantic errors in the generated models. The generated models are of small to medium size, with

<footnote n="2">²https://gitlab.telecom-paris.fr/mbe-tools/TTool/-/blob/master/src/main/java/atar translator/AvatarSyntaxChecker.java</footnote>

<footnote n="3">³https://github.com/ZebreDeSoixanteQuatorzeCanons/ModelGenerationWithFormalVerification</footnote>
<table><caption>Table 1. Practical evaluation. For each experiment, the syntax errors and properties are checked on the whole design model (the BD + all the SMDs). Red dots indicate cases where the feedback loop reached its maximum number of iterations without successfully correcting all remaining errors.</caption><thead><tr><th>Specification</th><th>Experiment 1</th><th>Experiment 2</th></tr></thead><tbody><tr><td>Ping-Pong Game</td><td>Time: 28 s<br>Safety verification loops: 1 (/20 allowed)<br>Tokens: 4,465<br>Cost: $0.06<br>Remaining syntax errors: 0<br>Unverified properties: 0 (/7 states)</td><td>Time: 9 min 20 s<br>Safety verification loops: 20 (/20 allowed)<br>Tokens: 78,245<br>Cost: $0.38<br>Remaining syntax errors: 0<br>Unverified properties: 4 (/8 states)</td></tr><tr><td>Pressure Controller</td><td>Time: 22 min 9 s<br>Safety verification loops: 20 (/20 allowed)<br>Tokens: 195,819<br>Cost: $0.87<br>Remaining syntax errors: 0<br>Unverified properties: 7</td><td>Time: 26 min 40 s<br>Safety verification loops: 20 (/20 allowed)<br>Tokens: 224,078<br>Cost: $1.19<br>Remaining syntax errors: 0<br>Unverified properties: 6 (/14 states)</td></tr><tr><td>Dynamic Positioning System</td><td>Time: 9 min<br>Safety verification loops: (4/4 allowed)<br>Tokens: 121,943<br>Cost: $0.59<br>Remaining syntax errors: 0<br>Unverified properties: 16 (/42 states)</td><td>Time: 9 min 12 s<br>Safety verification loops: (4/4 allowed)<br>Tokens: 127,157<br>Cost: $0.65<br>Remaining syntax errors: 0<br>Unverified properties: 20 (/39 states)</td></tr></tbody></table>

each model comprising in total between 2 and 9 blocks and 7 to 42 states.

Overall, the new mechanism excels at generating syntactically correct models: all models produced had zero remaining syntactic errors. In contrast, the previous version of TTool-AI frequently generated SMDs containing syntax issues. However, performance in terms of safety correctness remains more limited. Most states are reachable in the generated models but of the six experiments conducted, only one model satisfied all required properties. Further refinement of prompt engineering (particularly improving the feedback provided to the LLM regarding each unsatisfied property) would likely enhance the effectiveness of the auto-correction mechanism, on which we cannot conclude based on this first evaluation. It is worth noting, however, that the introduction of a safety properties verification loop that triggers up to 20 iterations statistically increases the likelihood of producing a design model with more verified properties, compared to the previous version of TTool-AI, which lacked such a loop.

The total execution time shows that the task is far from instantaneous, yet it remains negligible compared to the time a human would require to generate the same models for an equivalent to better quality, as previously demonstrated for other systems with a less performant feedback loop [3, 25]. Since up to 20 safety verification loops were allowed, each potentially containing up to 20 syntax verification sub-loops, verification failures have led to processing times of up to 26 minutes in our tests. On the other hand, simpler specifications, such as the first toy example, result in significantly faster executions, with models generated within half a minute. Despite these limitations and the inconclusiveness regarding the effectiveness of the safety auto-correction mechanism, the evaluation demonstrates a high level of success in correcting syntax errors, consistently producing syntactically valid SMDs. This represents a major step toward the formal verification of AI-generated models, since their syntactic correctness is the necessary condition to run model-checking algorithms.

## 5. CONCLUSION AND FUTURE WORKS

This work-in-progress paper introduces a new verification-driven feedback loop into TTool-AI, designed to improve the correctness of AI-generated design models with respect to both syntactic validity and compliance with safety properties. The approach relies on iterative algorithmic full syntax and model checking and refinement of LLM responses, progressively guiding the LLM toward increasingly accurate models. In its current implementation, initial experimental evaluations demonstrate excellent results for syntactic correctness, while also indicating that further refinement is needed to improve correctness with respect to safety properties. These evaluations do not enable indeed to conclude about the effectiveness of the safety auto-correction mechanism. Nonetheless, the fact that the new loop consistently produces syntactically correct, complete design models represents a highly promising first step towards more reliable AI-driven model generation. These improvements are achieved within reasonable execution times and at a very manageable monetary cost, making TTool-AI more applicable to real-world scenarios and use cases.

In addition to refining prompts to enhance the safety auto-correction feature, future work will aim to strengthen the integration of formal verification within the feedback loop, extending it beyond state reachability and deadlock-freedom to cover a broader range of properties. Our plan involves: (1) developing an LLM-based mechanism capable of automatically generating temporal logic properties that reflect the requirements, based on both the specification and the design model; and (2) integrating the verification of these properties into the feedback loop, enabling the generation of models that iteratively converges toward full compliance with the specification. This could also help to support a semi-automated certification process.

## REFERENCES

[1] Deniz Akdur, Vahid Garousi, and Onur Demirörs. A survey on modeling and model-driven engineering practices in the embedded software industry. *Journal of Systems Architecture*, 91, 2018.
[2] Charles André, S Cuccuru, Jean-Luc Dekeyser, Robert De Simone, Cédric Dumoulin, Julien Forget, Thierry Gautier, Sébastien Gérard, Frédéric Mallet, Ansgar Radermacher, et al. MARTE: a new OMG profile RFP for the modeling and analysis of real-time embedded systems. In *DAC Workshop UML for SoC Design*, pages 16–21, 2005.

[3] Ludovic Apvrille and Bastien Sultan. System Architects are not Alone Anymore: Automatic System Modeling with AI. In *Proceedings of the 12th International Conference on Model-Based Software and Systems Engineering - MODELSWARD'24. INSTICC, 2024. BEST PAPER AWARD*.

[4] Jordi Cabot. Vibe Modeling: Challenges and Opportunities. In *International Conference on Conceptual Modeling*, pages 105–118. Springer, 2025.

[5] Alessandro Tempia Calvino and Ludovic Apvrille. Direct model-checking of sysml models. In *9th International Conference on Model-Driven Engineering and Software Development*, pages 216–223. SCITEPRESS-Science and Technology Publications, 2021.

[6] Javier Cámara, Javier Troya, Lola Burgueño, and Antonio Vallecillo. On the assessment of generative AI in modeling tasks: an experience report with ChatGPT and UML. *Software and Systems Modeling*, 22, 2023.

[7] Eduardo Cibrián, José Francisco Olivert Iserte, Francesco Casella, Mario García Rodríguez, Jose María Alvarez-Rodríguez, and Juan Llorens. Automating Model Transformation from Modelica to SysML v2 with LLM-based Agents. *Available at SSRN 5564442*.

[8] Eduardo Cibrián, José Olivert-Iserte, Juan Llorens, and Jose María Álvarez-Rodríguez. An agent-based approach for the automatic generation of valid sysmlv2 models in industrial contexts. *Computers in Industry*, 172:104350, 2025.

[9] Edmund M Clarke, E Allen Emerson, and A Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. *ACM Transactions on Programming Languages and Systems (TOPLAS)*, 8, 1986.

[10] Matt Cotter, Aleksandra Markina-Khusid, Jyotirmay Gadewadikar, and Mike Hadjimichael. Applications of Artificial Intelligence to Model Based Systems Engineering: Initial Case Studies. In *2025 IEEE Aerospace Conference*, pages 1–7. IEEE, 2025.

[11] Gjalt de Jong. A UML-based design methodology for real-time and embedded systems. In *Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition*. IEEE, 2002.

[12] Pierre de Saqui-Sannes, Ludovic Apvrille, and Rob Vingerhoeds. Checking SysML Models against Safety and Security Properties. *Journal of Aerospace Information Systems*, 18(12):906–918, 2021.

[13] Juri Di Rocco, Davide Di Ruscio, Claudio Di Sipio, Phuong T Nguyen, and Riccardo Rubei. On the use of large language models in model-driven engineering. *Software and Systems Modeling*, 24, 2025.

[14] Alberto Ferrari, Leonardo Mangeruca, Orlando Ferrante, and Alessandro Mignogna. Desyreml: a sysml profile for heterogeneous embedded systems. In *Embedded Real Time Software and Systems (ERTS2012)*, 2012.

[15] Gábor Guta and Gábor Kusper. LLM-based framework to support the construction of valid formal models. 2025.

[16] Fernando Herrera, Héctor Posadas, Pablo Peñil, Eugenio Villar, Francisco Ferrero, Raúl Valencia, and Gianluca Palermo. The COMPLEX methodology for UML/MARTE Modeling and design space exploration of embedded systems. *Journal of Systems Architecture*, 60, 2014.

[17] Petri Kukkala, Jouni Riihimaki, Marko Hannikainen, Timo D Hamalainen, and Klaus Kronlof. UML 2.0 profile for embedded system design. In *Design, Automation and Test in Europe*, pages 710–715. IEEE, 2005.

[18] Shourong Lu and Wolfgang A Halang. A UML profile to model safety-critical embedded real-time control systems. In *Contributions to Ubiq-uitous Computing*, pages 197–218. Springer, 2007.

[19] Gabriel Pedroza, Ludovic Apvrille, and Daniel Knorreck. AVATAR: A SysML environment for the formal verification of safety and security properties. In *2011 11th Annual International Conference on New Technologies of Distributed Systems*, pages 1–10. IEEE, 2011.

[20] Jean-denis Piques. SysML for embedded automotive systems: SysCARS methodology. In *Embedded Real Time Software and Systems (ERTS2014)*, 2014.

[21] Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In *International Symposium on programming*, pages 337–351. Springer, 1982.

[22] Muhammad Rashid, Muhammad Waseem Anwar, and Aamir M Khan. Toward the tools selection in model based system engineering for embedded systems – A systematic literature review. *Journal of Systems and Software*, 106, 2015.

[23] Yves Roudier and Ludovic Apvrille. SysML-Sec: A model driven approach for designing safe and secure systems. In *2015 3rd International Conference on Model-Driven Engineering and Software Development (MODELSWARD)*, pages 655–664. INSTICC, 2015.

[24] Bastien Sultan and Ludovic Apvrille. AI-Driven Consistency of SysML Diagrams. In *Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems, MODELS '24*, page 149–159, New York, NY, USA, 2024. Association for Computing Machinery. ACM SIGSOFT DISTINGUISHED PAPER AWARD.

[25] Bastien Sultan and Ludovic Apvrille. TTool-AI: A Large Language Model-Based Assistant for Model Driven Engineering. *SN Comput. Sci.*, 6(7), October 2025. doi: 10.1007/s42979-025-04444-w. URL https://doi.org/10.1007/s42979-025-04444-w.

[26] Bastien Sultan, Léon Frénot, Ludovic Apvrille, Philippe Jaillon, and Sophie Coudert. AMULET: A Mutation Language Enabling Automatic Enrichment of SysML Models. *ACM Trans. Embed. Comput. Syst.*, 24(3), May 2025. ISSN 1539-9087. doi: 10.1145/3624583.

[27] Andreas Vogelsang, Tiago Amorim, Florian Pudlitz, Peter Gersing, and Jan Philipps. Should I stay or should I go? On forces that drive and prevent MBSE adoption in the embedded systems industry. In *Product-Focused Software Process Improvement: 18th International Conference, PROFES 2017, Innsbruck, Austria, November 29–December 1, 2017, Proceedings 18*. Springer, 2017.