论文部分内容阅读
采用基于属性的分析方法，对CTCS-3级列控系统需求规范进行形式化验证。首先建立UML模型并转换为PSL模型。然后通过仿真运行，不断修正该模型，得到可实现的PSL模型。最后运用验证工具对PSL模型进行相关属性的验证，通过反例对错误进行定位和修改。以需求规范中的模式转换为例，采用该方法对其可达性、转移性及死锁性进行验证，验证过程表明基于属性的分析方法适用于CTCS．3级列控系统需求规范的验证。