UPPAAi: Towards LLM-Assisted Modeling, Verification, Analysis and Synthesis

Peter Dolog; Kim G. Larsen; Marius Mikučionis; Frederik F. K. Rasmussen

cs.SEOct 29, 2026

UPPAAi: Towards LLM-Assisted Modeling, Verification, Analysis and Synthesis

Authors: Peter Dolog, Kim G. Larsen, Marius Mikučionis, Frederik F. K. Rasmussen

Organizations: Aalborg University, Aalborg, Denmark

Abstract

For more than three decades, UPPAAL has supported the modelling and analysis of real-time and cyber-physical systems. Yet building a suitable model, formalising the intended properties, choosing analysis techniques and interpreting counterexamples remain iterative tasks that demand substantial expertise. Large language models (LLMs) can offer plausible explanations and even solutions, but they are not necessarily correct. We present UPPAAI, an extension of UPPAAL in which users construct, explain, debug and specify models in dialogue with an LLM. The guiding principle is that the user requests, the LLM proposes, explains and orchestrates, and UPPAAL verifies. UPPAAI exposes the UPPAAL editor, queries and verifier through a Tools API. We report on seven case studies, from explaining to a newcomer to learning a controller, covering timed automata, stochastic hybrid automata and strategy learning. LLMs proved to be extremely helpful in not just generating solutions but also pro-actively suggesting relevant UPPAAL features it was not asked about.

Figures & tables

Panel of Figure 1 — Figure 1: The U PPAAI loop: the LLM generates, the model checker acts as the critic, and the user remains in control of the requirements and the model.

Figure 2: UML component diagram showing U PPAAL connecting to LLM Service through the langchain4j library via the LCMessages API, while a vendor-supplied Agentic Client connects via the LLMMessages API and reaches the U PPAAL tools through MCP.

Model and templates
Function	Description
getContext	The state of U PPAAL GUI (changes and selection)
get / replaceModel	Read or replace the whole model
checkSyntax	Check the model for syntax errors
getTemplateList	List the templates in the model
get / replaceTemplate	Read or replace a template

Table 1: Tools API: functions exposed by U PPAAL to the LLM.

API	Vendors & Environments
MCP	Anthropic Claude Desktop/Code, Mistral Vibe
Vendor Specific	OpenAI, Anthropic, Mistral AI
OpenAI	OpenAI, DeepSeek, Gemini, Grok, Groq, Ollama

Table 2: Tested support for LLM vendors

Case	Source	User’s task	Formalism; queries
Fischer’s mutual exclusion protocol	existing [ 11 , 1 ]	explore as newcomer; mutate & see what breaks	timed automata; safety, deadlock, leads-to
Box sorting on a conveyor belt	existing [ 8 ]	check that boxes are sorted; debug; scale up	timed automata, scalar sets; safety, reachability
Car lane maneuvering	existing [ 6 ]	fix a model in which two cars collide	timed automata with data; reachability, S MC
Spread of COVID-19	general knowledge ∗	model epidemic from scratch; convert	stochastic TA $\rightarrow$ CTMC $\rightarrow$ ODE; S MC
Storm water detention pond	requirements	synthesise a controller to maintain water level	stochastic hybrid game; strategy learning, S MC
Timing constraints in ATM network	general knowledge	model as newcomer, verify deadlines	timed automata; safety, sup bounds

Table 3: Overview of the case studies

Model Variant	timers	boxes	no B at end	no R off	deadlock $\rightarrow$ sorted	states
Original	1	2B/2R	$\times$	✓	–	–
Per-box timers	3	3B/3R	✓	✓	✓	–
Mutation: one timer	1	3B/3R	$\times$	$\times$	$\times$	–
Symmetric ∗	8	5B/3R	✓	✓	✓	20 160
Symmetric ∗	8	8B/3R	✓	✓	✓	69 745
Mutation: too few	4	5B/3R	$\times$	$\times$	$\times$	37 923

Table 4: Results: ✓ holds;

\times

violated; states: stored by verifyta ; – unchecked.

Purpose	Tools (calls)	Total
Inspect	getContext (5), getModel (2), getQueries (1), getTemplate (1)	9
Verify	verifyQueries (7)	7
Queries	insertQuery (18), removeQuery (12)	30
Edit	setGlobalDeclarations (4), checkSyntax (4), replaceTemplate (2), setSystemDefinition (2), replaceModel (1)	13
All	12 distinct tools	59

Table 5: U PPAAL MCP tool calls in the session.

Variant	$Q_{\max}$	avg level	P(overflow)	severity	P(below min)
random	60	0.47 m	$6.4\pm 4.0\,\%$	–	–
Opt	60	1.08 m	$3.6\pm 3.4\,\%$	0.30	94 %
random	120	0.22 m	${\leq}\,5\,\%$	–	–
Opt	120	1.32 m	$5.5\pm 3.9\,\%$	0.06	58 %
Opt reloaded	120	1.31 m	–	–	–

Table 6: Results per model variant over 24 h, random scenario (1000 runs, 95 % CI;

Q_{\max}

: fully open outlet flow in m 3 /min; severity in m

\cdot

min; –: not checked).

Purpose	Tools (calls)	Total
Inspect	getModel (5), getQueries (4), getContext (1)	10
Verify	verifyQueries (7)	7
Queries	insertQuery (8), removeQuery (6)	14
Edit	replaceModel (2), setGlobalDeclarations (2), checkSyntax (3), modifyLocation (1)	8
All	10 distinct tools	39

Table 7: U PPAAL MCP tool calls in the session.

Variant	deadline	window	overrun	WCRT	Pr	cex
CFG0 (shared window), $\Delta\leq 2$	✓	✓	✓	$46{+}\Delta$	0	–
CFG0, $\Delta=3$ (drifting offsets)	$\times$	✓ ∗	✓	133 (139)	0.032 (0.14)	51
CFG0, release jitter 11	$\times$	✓ ∗	✓	148	0.85	34
CFG1 (no isolation), $\Delta=0$	$\times$	$\times$	✓	46	0.50 §	54
CFG2 (time isolation), $\Delta\leq 2$ ; ${\leq}\,3$ losses	✓	✓	✓	38	–	–
BE, length-aware gates, or guard band 8	✓	✓	✓	48	0	–

Table 8: Results per model variant ( ✓ : holds;

\times

: violated; WCRT: exact worst-case latency; Pr: S MC probability of a deadline miss within 10 cycles; cex: steps of the shortest counterexample; –: not checked).

Purpose	Tools (calls)	Total
Inspect	getContext (2), getModel (2), getTemplateList (1), getQueries (1)	6
Verify	verifyQueries (2)	2
Edit	replaceModel (2), checkSyntax (3)	5
All	7 distinct tools	13

Table 9: U PPAAL MCP tool calls in the session.

Figure 3: Fischer process template P with parameter pid .

Model Variant	mutex	no deadlock	req $\leadsto$ wait	req $\leadsto$ cs
Original	✓	✓	✓	$\times$ (4, “lazy”)
x > k $\to$ x > = k	$\times$ (6)	–	–	–
no invariant on req	✓	$\times$ (6)	$\times$ (1)	–
eager variant ∗	✓	✓	✓	$\times$ (15, lasso)

Table 10: Results: ✓ holds;

\times

violated, with counterexample length; – unchecked.

Purpose	Tools (calls)	Total
Inspect	getModel (3), getQueries (2), getContext (2), getVerificationOptions (1)	8
Verify	verifyQueries (11), getQueryTrace (5)	16
Queries	setQueryOption (9), insertQuery (1), removeQuery (1)	11
Edit	modifyEdge (5), modifyLocation (4), addEdge (2), addLocation (1), setGlobalDeclarations (1), replaceModel (1), checkSyntax (1)	15
All	16 distinct tools	50

Table 11: U PPAAL MCP tool calls in the session.

Case	Pr.	Calls	Obtained with UPPAAi	Beyond the request	Reference
Debugging an existing model
Belt	4	59	bug suspected at once and confirmed by UPPAAL; explained from the trace; fixed with one timer per black box; final model verifies in seconds	bound of at most 8 boxes on the belt; state-space explosion diagnosed; scalar sets for symmetry reduction	model never taken this far by us; session of 17 min
Lanes	12	56	two bugs found with UPPAAL, explained and fixed; SMC guarantees for the full model with more lanes and cars, in a full sweep	lanes shortened (700 $\to$ 120) to fit the state space	buggy left-over; unresolved after repeated half-hour attempts
Known domain
COVID	6	51	agent-based model (one automaton per individual), fully parameterised; SMC queries in correct syntax; CTMC and ODE variants	clean-up of previous session; extensions (age structure, threshold-triggered lockdown or vaccination, hospital capacity); consistency of the three models shown	agent-based model was the end goal of our earlier work [ 9 ]
Pond	12	39	Stratego model with randomised rain scenarios and ODE pond dynamics; learned periodic outlet controller balancing overflow against average level	previous model saved and cleared; step-size study with Stratego to shorten learning	complete model and controller in one session

Table 12: The sessions side by side, emphasising acceleration (Pr.: prompts; Calls: MCP tool calls; Beyond the request: contributions the user did not ask for; Reference: what had been achieved, or what the user knew, without the LLM).

Appendix figures & tables7 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 4: Claude prompt, result and explanations

Panel of Figure 5 — Figure 5: Claude created traffic lights model with queries through U PPAAL MCP

Figure 6: U PPAAL with direct connection to Anthropic API with Claude Sonnet 5.5

Figure 7: Configuring U PPAAL MCP connection (Fig. 8(b) ) within Claude Desktop

Panel of Figure 8 — Figure 8: LLM configuration dialogs in U PPAAL

Ingredient	Example syntax	Role
Locations	Idle , Busy	Control states. Initial, urgent (no delay) and committed (atomic, no interleaving) variants
Clocks	clock x , y ;	Real-valued, advancing at rate 1 . Stopwatches via rate constraints x ’==0
Hybrid / ODE dynamics	T ’ == - k *( T - Tenv )	Continuous variables with arbitrary rates or ODEs written as derivative constraints in invariants, using double variables and maths functions. These give stochastic hybrid automata, analysed by simulation and S MC ; the symbolic engines support only stopwatches
Invariants	x < = 5	Location constraint bounding how long time may pass there
Edges	g / sync / upd	Guard, optional synchronisation and update (clock resets, assignments, function calls), with select for families of edges
Clock constraints	x - y < 3	Bounds on clocks and clock differences, in guards and invariants

Appendix

Table 13: Ingredients of a U PPAAL modeling language.

Formalism	Non-determinism	Typical queries	Results produced
Timed automata (symbolic MC)	Non-deterministic: all behaviours are explored exhaustively	E < > p , A [] p , E [] p , A < > p , p $-$ $-$ > q , A [] not deadlock , sup / inf / bounds { p }: e	Boolean verdict (“maybe” for stopwatch over-approximation). Symbolic diagnostic trace (witness or counterexample). Upper and lower bounds
Stochastic (hybrid) TA (SMC)	Probabilistic: uniform or exponential delays, weighted branches, race between components	Pr [ < = T ]( < > p ) , Pr [ < = T ]( < > p ) > = 0.9 , Pr .. > = Pr .. , E [ < = T ; n ]( max : e ) , simulate [ < = T ; n ]{ e1 , e2 }	Probability estimates with confidence intervals. Hypothesis-test and comparison verdicts. Expected values with confidence intervals. Sampled trajectories, histograms and concrete witness traces
Timed games (TIGA)	Antagonistic environment controls the uncontrollable edges	control : A [] p , control : A < > p	Verdict, plus a synthesised most permissive winning strategy that is correct by construction
Timed MDPs (Stratego)	Stochastic environment, controller chooses	strategy S = minE ( e )[ < = T ]: < > p under Safe , Pr [..]( < > p ) under S , E [..]( max : e ) under S , simulate [..]{..} under S	Near-optimal strategies learned by reinforcement learning, optionally shielded by a synthesised safe strategy. Strategies can be evaluated, compared and model checked

Appendix

Table 14: Formalisms, queries and results supported by U PPAAL 5.0.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 345 papers

ExVerus: Verus Proof Repair via Counterexample Reasoning
Mar 26, 2026Jun Yang, Yuechun Sun, Yi Wu +5Formal Verification
The University of Chicago · Purdue University · The University of Toronto +1
Early-Stage Product Line Validation Using LLMs: A Study on Semi-Formal Blueprint Analysis
Apr 22, 2026Viet-Man Le, Thi Ngoc Trang Tran, Sebastian Lubos +2Software Engineering LLM Evaluation
Graz University of Technology Graz, Austria
AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
Apr 24, 2026Pouya Pezeshkpour, Estevam HruschkaLLM Evaluation LLM Answer Verification
Megagon Labs

Mar 26, 2026J/K move · Enter open · S save

ExVerus: Verus Proof Repair via Counterexample Reasoning

Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad+4

The University of Chicago · Purdue University · The University of Toronto+1

Formal Verification

Open paper AskPDF arXiv

Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present EXVERUS, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.

Abstract

Formal Verification

Explore similar work

ExVerus: Verus Proof Repair via Counterexample Reasoning

Early-Stage Product Line Validation Using LLMs: A Study on Semi-Formal Blueprint Analysis

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs