Tools

Interlocking Model

Contributors
Christophe Limbrée, Simon Busard
Tags
, ,

To link papers to this page, give a list of papers ids in the References field. (Same mechanism as the Research Themes pages)

nameche08.smv is the NuSMV model of the station of Namêche in Belgium. This model was developed by Christophe Limbrée in the framework of his PhD's thesis.

NuSMV is a reimplementation and extension of SMV symbolic model checker, the first model checking tool based on Binary Decision Diagrams (BDDs). 

 LTSA is available from the LTSA home page.

This model features :

  • Fourteen routes.
  • The simulation of two trains.
  • The track components like: points, track circuits, treadles.
  • 132 invariant properties.

The model is based on the application data of the real interlocking (SSI) controlling the station.

The model is provided as a zip file. It has been tested with NuSMV version 2.5.4.

Download Namêche station NuSMV model

The model can also be analyzed and tested with a checker specially developed to verify such kind of NuSMV models. The checker is implemented in Python 3.x with PyNuSMV. The checker, as well as the version of PyNuSMV it is based on, are available:

If you want to add an historic, giving older versions, etc, you can do it here.

Contributor(s)
Christophe Limbrée, Simon Busard

Related Publications:

Tags Tags: , ,