| Kurzfassung
|
To ensure that a system satisfies its requirements, Model Checking can be used. To be able to perform Model Checking, the requirements first need to be translated from Natural Language (NL) into a formal logic, like Computation Tree Logic (CTL). Automating this translation task would be beneficial, since it is a time consuming and error-prone process. Existing research has shown that Large Language Models ( LLMs) can at least partly automate this task. A notable gap in existing research is the lack of an evaluation of how an LLM performs at translating the requirements of previously unseen projects into CTL. To fill this gap, I first annotated an existing dataset of NL requirement to CTL translations with the source project of each requirement. Subsequently, I used this dataset to evaluate how different LLMs perform at this translation task on unseen projects using different prompting techniques. I also evaluated the performance of one fine-tuned LLM on this task. The best of the approaches translated 73% of NL requirements accurately, which shows that, while not perfect, an LLM can be helpful in aiding with the translation of NL requirements to CTL, even on unseen projects.
|
