Can Large Language Model Aid in Generating Properties for UPPAAL Timed Automata? A Case Study

Real-time systems play an important role in nu-merous industries, including automobiles, telecommunications, medical systems, among others. When designing these systems, we must consider strict timing constraints and operational logic to ensure the correctness and safety during their operation. Model checking is an effective method to bridge the gap between high-level system requirements and formal verification processes. However, practitioners are often requested to have a profound understanding of the system in order to write properties for verification as comprehensively as possible. In this paper, we investigate the potential of utilizing a large language model, G PT-4, to aid in generating properties for the UPPAAL timed automata model. This is accomplished through the reconstruction of the time automata of a classic industrial real-time system concerning a gear controller. We employ four design settings to prompt the model, meticulously inspect and categorize the generated properties, and manually rectify any syntax errors to facilitate verification using UPPAAL. The experimental findings reveal that GPT-4 can generate properties akin to those conceived by humans in 10.3% of cases. Despite exhaustive human-crafted properties, GPT-4 still generates 6 additional properties alongside the 46 human-crafted ones. Notably, GPT-4 can generate new properties even without system requirements, solely relying on provided UPPAAL timed automata and examples of human-crafted properties. However, syntax errors in GPT-4 generated properties are high at 82.5 %, while illogical properties are relatively low at 12.5 %.