属性驱动的列车控制系统需求建模与验证

Property-driven modeling and verification for requirements of Train Control System

形式化语言越来越多地用来描述列车控制系统需求规范,其精确的语法和语义一方面有助于创建精确的需求模型、消除理解差异,另一方面也为进一步分析验证提供了基础。通过提出一种基于属性的需求分析方法,利用具体的形式化技术来分析需求。首先将由自然语言描述的需求规范转换为属性描述语言(PSL)形式化规范,并通过仿真和博弈分别进行语义检查和可实现性验证,最后通过断言来检验形式化语言所刻画的系统的精确性和完整性。该方法从自然语言形式的需求约束中直接提取相关需求规范,构造形式化模型并进行验证,为需求的早期确认提供了一种新的实用途径。并以CTCS-3级列控系统RBC切换场景为例,说明该方法的有效性。

Formal languages were increasingly used to describe the requirements specification of Train Control System, the precise syntax and semantics on the one hand, helped to create accurate demand model, eliminated understanding differences, on the other hand also provided a basis for further analysis of the validation. This paper presented a property based requirements analysis approach which analyzed requirement by the application of specialized formal analysis techniques. Firstly, requirements described by natural language were transformed into formal requirements described by PSL （Property Specification Language）. Secondly, the semantics were checked by simulation and the realizability of the System was verified by the game. Finally, the correctness and completeness of the System were validated by assurance. This method directly extracted the relative requirements specification from requirement constraints described by natuxal language and formalized the structures model to verify, also provided a new practical way for the early validation of the requirements. By using some requirement fragments from RBC Handover scenarios of CTCS-3 Train Control System as a realistic example, it was demonstrated the effectiveness of this approach.