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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

LLM-Enhanced SysML Formal Method for Flanking Protection in Train Autonomous Control System

  • Qian Xu,
  • Lei Zhang,
  • Tengfei Li,
  • Xiaoyong Wang

摘要

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.