Can Large Language Models Support Modeling Systems with ASMETA? A Case Study with a Planetary Rover

Formal modeling languages provide strong support for the specification, analysis, and validation of cyber-physical systems, but their adoption in practice is often hindered by the effort and expertise that are required to produce correct and complete models. In this paper, we investigate whether Large Language Models (LLMs) can support the modeling process by assisting in the generation and refinement of ASMETA specifications from natural language requirements. We propose an iterative and human-in-the-loop workflow in which an LLM is used to derive an initial ASMETA model, progressively refine it, and support scenario-based validation using existing ASMETA tools. The approach explicitly combines automated assistance with human inspection to mitigate modeling errors and potential biases introduced by the LLM. We evaluate the feasibility and effectiveness of this workflow through a case study based on the ABZ 2026 planetary rover problem, using GPT-5.2, accessed via the ChatGPT interface and leveraging the Projects functionality to support persistent and multi-iteration interactions. Our experience suggests that LLMs can significantly lower the entry barrier to formal modeling and support engineers by accelerating the creation of analyzable ASMETA artifacts, but expert oversight is necessary to ensure correctness, completeness, and alignment with stakeholder intent.