LLM-Enhanced SysML Formal Method for Flanking Protection in Train Autonomous Control System
摘要
Formal methods offer a rigorous and systematic approach to ensuring the safety, reliability, and efficiency of Communication-based Train Control (CBTC) systems during the design and development phases. However, the high level of abstraction in formal methods presents challenges, such as difficulty in modeling and the risk of omissions and errors. The fine-tuning capability of large language models (LLMs) after pre-training has attracted attention for addressing these challenges, particularly when integrating LLMs with formal methods. The Train Autonomous Control System (TACS), transforming from the ground-centric feature in CBTC to the train-centric feature, introduces significant innovations, including the Flanking Protection Function. Firstly, the architecture of the TACS system is analyzed as well as the requirements for the flanking protection function. Then, it proposes a four-step LLM-SysML framework, which includes requirements collection and analysis, LLM-assisted element abstraction, SysML model implementation, and performance assessment. Finally, three SysML models are developed using commercial LLM tools, i.e., use case diagram, sequence diagram and requirement diagram. Results demonstrate that LLM-SysML offers higher accessibility and fewer false alarms compared to traditional manual modeling approaches.