Model checking techniques applied to the verification of railway interlocking systems may fail to scale. Compositional methods have been proposed to reduce the size of networks to be model checked. In this paper we extend the scope of a previously defined compositional method to systems employing flank protection, not supported in the original method because flank protection requires a coordination of distant points. The extension comprises soundness results for this new context and a decomposition strategy able to divide a network into sub-networks of minimal size.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Compositional Model Checking of Railway Interlocking Systems Featuring Flank Protection

  • Anne E. Haxthausen,
  • Alessandro Fantechi,
  • Gloria Gori

摘要

Model checking techniques applied to the verification of railway interlocking systems may fail to scale. Compositional methods have been proposed to reduce the size of networks to be model checked. In this paper we extend the scope of a previously defined compositional method to systems employing flank protection, not supported in the original method because flank protection requires a coordination of distant points. The extension comprises soundness results for this new context and a decomposition strategy able to divide a network into sub-networks of minimal size.