铁路通信信号工程技术2026，Vol.23Issue(3)：9-14,6.DOI:10.3969/j.issn.1673-4440.2026.03.002
基于大模型的形式化验证系统架构设计
Architecture Design of Formal Verification System Based on Large Language Models
摘要
Abstract
As train control systems are complex industrial control systems,achieving security verification and intrinsic security throughout the lifecycle of train control systems remains a significant challenge.Conducting security verification on the codes during the development of train control systems will help understand the security status of the system and facilitate the timely patching of vulnerabilities.To address the need for cybersecurity verification in train control systems,this paper proposes the architecture of a large language model-based formal verification system for cybersecurity.By combing large language models with formal verification tools,this system leverages the deep semantic understanding and reasoning capabilities of large language models to automatically capture,meticulously decompose,and formally model the complex cybersecurity requirements of train control systems.This ensures that every security specification and service requirement can be accurately and executably represented.Additionally,by integrating multiple advanced verification techniques and verification tools,this system employs intelligent strategy scheduling and parallelized verification execution to quickly deliver quantitative conclusions on system security and examples of reproducible error.This enables an intelligent verification process encompassing"security requirements,verification decision,and result feedback".关键词
大模型/安全验证/形式化验证/智能验证Key words
large language model/cybersecurity verification/formal verification/intelligent verification分类
信息技术与安全科学引用本文复制引用
陈红学,马卫红,杨雅涵,申翔宇..基于大模型的形式化验证系统架构设计[J].铁路通信信号工程技术,2026,23(3):9-14,6.基金项目
国家重点研发计划项目(2024YFB3108600) （2024YFB3108600）
