数据集概述
该数据集为论文《Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect》的补充数据，包含UMC和Sparx Enterprise Architect相关的实验文件，涉及模型文件、代码、日志、文档等，支持铁路领域形式化验证与模型开发研究的实验复现。
文件详解
- 文档类文件：
- README.pdf：PDF格式，提供数据集说明文档
- SPARX_diagram_report.pdf：PDF格式，Sparx模型的图表报告
- UMC-SeqDiagSmall.pdf：PDF格式，UMC场景的简化序列图
- UMC-SeqDiagComplete.pdf：PDF格式，UMC场景的完整序列图
- 文本类文件：
- UMC-Scenario0+mutation.txt：TXT格式，UMC场景0及变异配置信息
- SPARX_simulation_log.txt：TXT格式，Sparx模型的仿真日志
- 视频文件：
- experiments reproduction video.flv：FLV格式，实验复现视频
- 模型文件：
- SPARX_model.eapx：EAPX格式，Sparx Enterprise Architect模型文件
- SPARX_model.xmi：XMI格式，Sparx模型的XMI导出文件
- 代码压缩包：
- SPARX_generated_code.zip：ZIP格式，Sparx模型生成的代码压缩包
适用场景
- 铁路系统开发研究：分析形式化验证与基于模型开发在铁路领域的应用
- 软件工程实验复现：基于提供的模型、代码和日志复现相关实验
- 模型工具集成研究：探索UMC与Sparx Enterprise Architect工具的互补性
- 形式化方法应用：研究铁路系统中形式化验证技术的实践效果
