分析大型强子对撞机紧凑μ子螺线管实验的控制软件
计算机科学中的逻辑
2013-03-04 v1 软件工程
摘要
欧洲核子研究中心紧凑μ子螺线管实验的控制软件包含超过30000个有限状态机。这些状态机按层次组织：命令向下发送，状态变化向上发送。系统的庞大规模使得在宏观层面完全理解其行为的细节几乎不可能。微观层面已经存在的模糊性加剧了这一问题。我们通过使用mCRL2进程代数形式化描述有限状态机，解决了后一个问题。该翻译已使用ASF+SDF元环境实现，并通过单个有限状态机的模拟和可视化以及控制软件子系统的形式化验证评估了其正确性。基于有限状态机的形式化语义，我们开发了专用工具，用于检查可在孤立有限状态机上验证的属性。
引用
@article{arxiv.1101.5324,
title = {Analysing the Control Software of the Compact Muon Solenoid Experiment at the Large Hadron Collider},
author = {Yi-Ling Hwong and Vincent J. J. Kusters and Tim A. C. Willemse},
journal= {arXiv preprint arXiv:1101.5324},
year = {2013}
}
备注
To appear in FSEN'11. Extended version with details of the ASF+SDF translation of SML into mCRL2