UPPAAL gains interactive help from large language models for system modeling
UPPAAi: Towards LLM-Assisted Modeling, Verification, Analysis and Synthesis
Software EngineeringArtificial IntelligenceLogic in Computer Science
Summary
Modeling complex systems like timed or hybrid automata can be hard and often requires expert knowledge. The authors created UPPAAI, a tool that integrates a large language model (LLM) with the existing UPPAAL software to help users build, explain, and check these models through a conversation. The LLM suggests and explains steps while UPPAAL verifies correctness, making model building more approachable and interactive. This new tool was tested on different case studies, showing that LLMs can proactively offer helpful features even when users don’t ask for them.
What this means in practice
- •For embedded systems developers: Build and verify real-time system models interactively with LLM guidance and UPPAAL’s verification to improve design accuracy.
- •For control systems engineers: Use dialogue with LLM-assisted tools to learn and synthesize controllers for hybrid and timed systems more efficiently.
- •For software development toolmakers: Create advanced, interactive modeling environments by integrating LLMs with formal verification software like UPPAAL.$Commercial implications: Enables new AI-powered formal verification products that improve user experience and broaden customer base.
Authors
Peter Dolog, Kim G. Larsen, Marius Mikučionis, Frederik F. K. Rasmussen
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.