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

1 Introduction

• UPPAAI uses UPPAAL as a sound, exhaustive critic because plausible LLM-generated artefacts do not establish correctness for subtle concurrency, synchronisation, and real-time requirements.The introduction notes that external evaluators can drive repair loops, whereas LLM self-evaluation is unreliable.Source: §1 · p. 1
• The loop lets users construct, explain, debug, and specify models in dialogue, with UPPAAL verdicts and counterexamples guiding refinement.It also supports quantitative questions through UPPAAL SMC and controller learning through UPPAAL STRATEGO.Source: §1 · p. 2
• The intended benefit is to make model checking useful for requirements engineering, architecture exploration, and teaching, beyond late-stage validation.A validated UPPAAL model can serve as a semantic anchor for testing generated code for conformance or synthesising controllers.Source: §1 · p. 2
• Verification of a model does not verify the real system: an LLM can build the wrong abstraction or weaken a query until it passes.The user can inspect and edit changes, and a property can be tested against a deliberately broken model variant.Source: §1 · pp. 2–3
• UPPAAI exposes model editing, query management, and verification through a Tools API, with embedded-chat and external-agent workflows.The contribution also describes embedded chat via langchain4j and an external agentic client via MCP.Source: §1 · p. 3
• The paper reports seven case studies and discusses when UPPAAL corrected the assistant, which claims relied on argument rather than tool results, and interface limitations.The cases span timed and stochastic models, ODEs, and strategy learning.Source: §1 · p. 3

Modelling

• A UPPAAL model is a network of timed automata instantiated from parameterised templates and enriched with discrete data and C-like code.The same syntax supports four interpretations that differ in how non-determinism is resolved, each with its own queries and result type.Source: §2 · p. 3

Tools integration

• The component diagram connects UPPAAL to LLM services through langchain4j and LCMessages, or through a vendor client using LLMMessages and MCP.The two messaging APIs exchange requests and replies with an LLM.Source: Figure 2 · p. 4

Specifications

• UPPAAL specifications cover reachability, safety, liveness, deadlock freedom, probabilistic and expected-value questions, and strategy synthesis and analysis.SMC queries can be bounded by time, steps, or cost.Source: §2 · p. 4

• Two messaging APIs support the integration: the vendor's RESTful LLMMessages API and langchain4j's Java LCMessages API.langchain4j also offers MCP access to external clients and handles function-call encoding and decoding.Source: §3 · pp. 4–5

Workflow A: external Agentic Client

• Workflow A leaves history and context with an external client, which resends the conversation and may need extra tool calls to learn what the user is viewing.The client can remain a familiar agentic environment, while the Tools API itself is sandboxed to UPPAAL functions.Source: §3 · p. 5

Workflow B: embedded UPPAAL chat

• Workflow B gives UPPAAL ownership of the chat history and lets it attach information such as the user's current selection to each request.langchain4j handles tool calls and returns their results to the LLM until it produces a reply.Source: §3 · p. 5

• Both workflows end at the same Tools API, but differ in who initiates requests and controls how context reaches the LLM.The external client reuses an existing interface but must retrieve or inject context; embedded chat gives UPPAAL prompt control at the cost of a custom chat implementation.Source: §3 · pp. 5–6
• The Tools API groups functions for editing models and templates, managing queries, and running and inspecting verification; simulation and version-control features are planned.Source: §3 · p. 6, Table 1 · p. 6

4 Case Studies

• Across seven cases, the study covered timed and stochastic models, hybrid clocks, and strategy learning, with summary reports for four cases.The cases included existing models and models built from scratch, for users ranging from newcomers to experienced modellers.Source: §4 · p. 7

4.1 Red/Black Box Sorting on a Conveyor Belt

• Five named black-box instances timed out, while scalar sets enabled symmetry reduction and verification in 3 s.A single timer lost ejects; per-box timers and scalar sets were used, and the intended final state was reachable in all checked variants.Source: §4.1 · pp. 8–9

4.2 Storm Water Detention Pond

• Doubling the pond’s open outlet raised the level by 0.24 m and cut overflow severity 5×.Extreme rain at 180 m3/min exceeded the open outlet, making overflow unavoidable at the original capacity.Source: §4.2 · p. 10

4.3 Robustness of TSN Gate Schedules (IEEE 802.1Qbv)

• The TSN analysis found 2/64 failing offset combinations, versus Claude’s predicted 1/64; SMC estimated [0.027, 0.038] at ∆=3.Exhaustive checking found a second failure involving a late switch with latency 49 > 48; three SMC variant defects also contradicted results or predictions.Source: §4.3 · p. 11
• In TSN checks, correlated per-node offsets remained robust up to δ=2, while independent per-event jitter reported violations even with perfect clocks.Without isolation, the schedule failed with perfect clocks; guard band 7 still left a rare event in 3/2000 runs, found exhaustively in 0.5 s.Source: §4.3 · p. 12

4.4 Fischer’s Mutual Exclusion Protocol

• Removing the x≤k guard on req did not break mutual exclusion because the edge guard remained, although deadlock freedom and req⇝wait failed.The model checker’s verdicts corrected the assistant’s prediction.Source: §4.4 · p. 13
• In Fischer’s protocol, changing a comparison exposed a mutual-exclusion race exactly at x=k, and a leads-to failure required refinement to expose starvation.The race counterexample took 6 steps and 0.007 s; the first liveness counterexample arose because the winning process could idle in wait.Source: §4.4 · p. 13

Debugging existing models

• For existing models, Claude found and fixed bugs, explained counterexamples, and used model reductions to make verification tractable.In the lane-change case, it shortened lanes from 700 to 120 and swept the full model with SMC.Source: §5 · p. 14

Known domains

• In known domains, Claude produced a COVID-19 agent-based model with SMC queries, consistent CTMC and ODE variants, and a learned detention-pond outlet controller.For the pond, it used STRATEGO to find a suitable ODE step size when learning slowed.Source: §5 · p. 14

New domains

• In new domains, Claude built a high-quality-looking TSN model from a paper and user-suggested architecture, while an engineer new to timed automata obtained a verified ATM model.Claude explained TSN templates and proposed experiments and SMC queries; UPPAAL refuted some predictions, which Claude explained.Source: §5 · p. 14

Teaching

• For teaching, Claude recognized Fischer’s protocol, proposed experiments, and prepared a starvation-loop counterexample in the simulator with little learner effort.It accepted UPPAAL’s refutation of its own prediction.Source: §5 · p. 14

Potential pitfalls/misunderstandings

• Brief, generic questions can elicit generic answers that are only superficially tailored, leaving speculative proposals unchecked until a specific case exposes a mismatch.The authors note that users may not request checks at the time, so the mismatch can emerge later.Source: §5 · pp. 14–16

Potential information leaks

• A local MCP agent can access local resources, creating information-leak risk; remote LLM APIs instead limit agent access to the Tools API.In the TSN case, Claude Code searched the computer for verifyta and used it to sweep parameters outside the UPPAAL workspace.Source: §5 · p. 16

Overall

• Models and queries were judged high quality, with substantial productivity gains and unrequested suggestions, but fidelity to real systems remained for domain experts to judge.Each case was a single session, so these are the authors’ judgments rather than measurements.Source: §5 · p. 16

Contribution

• UPPAAI adds a Tools API for LLMs to construct, explain, debug, and specify models through an external MCP client or embedded UPPAAL chat.In case studies, the assistant fixed long-standing bugs, built models in unfamiliar domains, and suggested unrequested features and analyses.Source: §6 · p. 16

Interface constraints

• The interface still lacks cancellable, non-blocking verification, default access to several analysis tools, variant verification, undo-preserving replacement, and model-stored learned strategies.Minute-long verification and learning runs can stall the session.Source: §6 · p. 16

Evaluation scope

• Because each case was one session with one LLM, the authors plan provider comparisons, repeated sessions, and studies with a wider user group.The session files are publicly available.Source: §6 · p. 16

Claude Code with MCP

• The MCP workflow starts in Claude Desktop by selecting Claude Code, configuring UPPAAL MCP, and prompting for a traffic-control model with suitable phase timings.Fig. 4 is captioned as showing the Claude prompt, result, and explanations.Source: A Demo using Anthropic Claude Code… · p. 19, Figure 4 · p. 19

Model and query inspection

• While Claude works through the UPPAAL Tools API, the editor displays the model and the UPPAAI panel shows the interaction history; the verifier displays checked queries.The demo text describes comments in the declarations and explanations for each query.Source: A Demo using Anthropic Claude Code… · p. 20, Figure 5 · p. 20

Direct API connection

• Alternatively, UPPAAL can use an Anthropic API key with Claude Sonnet 5.5, but results may vary because LLMs are nondeterministic.The accompanying figures are captioned as showing the API connection and LLM configuration dialogs.Source: A Demo using Anthropic Claude Code… · pp. 21–22, Figure 6 · p. 21, Figure 7 · p. 21

Modeling language

• Table 13 presents the ingredients of the UPPAAL modeling language.Source: Table 13 · p. 23

Query languages

• Table 14 presents the formalisms and queries supported by UPPAAL 5.0.Source: Table 14 · p. 24

Results

• Table 14 also covers the results supported by the listed formalisms.Source: Table 14 · p. 24