NL2CSP: Towards Automated CSP Code Generation with Large Language Models

Communicating Sequential Processes (CSP) is a formal language used in modeling and verifying concurrent systems and protocols. However, manually constructing a CSP model is typically time-consuming. Recent advancements in Large Language Models (LLMs) show potential for automatically transforming requirements in natural language into formal specifications. In this paper, we propose the first datasets of CSP: CSP#-PAT-84 and CSP#-Handwrite-45, containing a total of 129 models and 1375 processes in a machine-readable syntax CSP#. The CSP#-PAT-84 dataset comprises CSP models from examples in the Process Analysis Toolkit (PAT) and covers five categories. The CSP#-Handwrite-45 dataset consists of CSP models extracted from research papers focusing on practical protocols, algorithms, and systems. Moreover, we introduce NL2CSP, a multi-stage approach designed to improve the performance of LLMs in generating codes in CSP#. Experiments are conducted on both the process generation and model generation tasks to evaluate the capability of LLMs to generate correct CSP processes and models, as well as to establish a benchmark for future research. The results demonstrate that with the capability of in-context learning, LLMs can understand most of the requirements written in natural language and generate corresponding CSP processes and models.