数据集概述
本数据集包含FormaSig项目中EULYNX Point接口的mCRL2模型、μ-演算公式需求文件及测试相关工件，用于支持研究结果的复现。数据涵盖特定点接口和通用PDI接口的模型、对应需求文件、测试模型、状态空间文件、测试日志及模拟器源代码，共20个文件。
文件详解
- mCRL2模型文件
- 文件名称：point_spec.mcrl2、pdi_spec.mcrl2、mbt.mcrl2
- 文件格式：.mcrl2
- 字段映射介绍：point_spec.mcrl2为点特定模型，pdi_spec.mcrl2为通用PDI接口模型，mbt.mcrl2为测试相关模型
- 需求文件
- 文件名称：REQ_P_001.mcf、REQ_P_001_1.mcf、REQ_P_002.mcf等12个.mcf文件
- 文件格式：.mcf
- 字段映射介绍：REQ_P_开头文件对应point_spec.mcrl2模型需求，REQ_PDI_开头文件对应pdi_spec.mcrl2模型需求
- 测试辅助文件
- 文件名称：rename_file.re
- 文件格式：.re
- 字段映射介绍：用于将内部动作重命名为tau的重命名文件
- 状态空间文件
- 文件名称：partial_state_space.aut、partial_state_space_reduced.aut
- 文件格式：.aut
- 字段映射介绍：分别为mbt.mcrl2模型的部分状态空间及弱跟踪互模拟约简后的状态空间
- 压缩文件
- 文件名称：test-logs.zip、Simulator code.zip
- 文件格式：.zip
- 字段映射介绍：test-logs.zip为测试日志，Simulator code.zip为模拟器和测试工具的源代码
数据来源
FormaSig项目
适用场景
- 铁路信号接口形式化验证：基于mCRL2模型和μ-演算需求，验证EULYNX Point接口的正确性
- 模型测试复现：利用测试模型、状态空间文件和测试日志，复现EULYNX接口的测试过程
- 形式化方法研究：分析mCRL2模型在铁路信号系统中的应用效果与优化方向
- 模拟器开发参考：基于Simulator code.zip的源代码，开发或改进EULYNX接口的测试模拟器
