摘要
结合统一建模语言UML与符号模型检验SMV形式化方法,提出需求规范严格建模和验证方法。利用需求管理工具,保证了模型和规范的一致性和对规范的覆盖性,同时实现了规范验证结果对模型、转换规则和规范的跟踪。给出了CTCS-3级列控系统严格建模与验证的方法体系和流程,并以CTCS-3级列控系统需求规范中的模式转换部分为例,说明了规范的建模、验证和分析过程。
Through combine the Unified Modeling Language and Symbolic Model Checking,which is a formal verification method,we propose a rigorous modeling and verification method. By using requirement management tool,we ensure the consistency between the specification and the model and a complete coverage of the model over the specification. We also realize the tracking of the results. In addition,we propose the methodology and process of rigorous modeling and verification of CTCS-3 system specification. Taking the portion of pattern conversion in CTCS-3 system requirement specification as example,we demonstrate the whole process of modeling,verification,and analysis.
出处
《铁道通信信号》
2010年第4期7-12,共6页
Railway Signalling & Communication
关键词
CTCS-3级列控系统规范
符号模型检验
严格建模和验证
CTCS-3 system requirement specification
Symbolic model checking
Rigorous modeling and verification
