Interlocking formal design solution


Interlocking systems design and validation require managing both safety and efficiency.IXL interlocking
IXL Builder is Systerel’s computer based interlocking design solution.
It implements a certifiable design and deployment process based on the extensive use of formal methods.

Systerel IXL Builder helps to automate and coordinate design, safety assessment and functional validation.

It offers an evolutive and modular range of certifiable solutions that can be tailored to each process.

Typical workflow

  1. Model a generic design using an OO paradigm focused on class and state machine diagrams
  2. Deploy the design over imported configuration data
  3. Formally assess th safety of the instantiated design
  4. Validate the design with host simulation
  5. Generate code and certify it
  6. Replay the validation with the hardware in the loop



Generic Design

  • Generic IXL modeling using an object oriented paradigm focused on class and state machine diagrams
  • Export model documentation

Deployment Design

  • Import data from external data preparation tools
  • Non vital track layout editor available for editing test data

UML State Machine modeling environment

Safety Assessment

  • Translation of vital requirements into proof obligations based on model elements
  • Formally proved design achievement
    • Counterexample interpretation
    • Design issue identification
    • Proof obligations and environment constraints model adjustment

IXL interlocking
Animating signaling rules

Functional validation

  • Generic tests instantiated according to track description
  • Host functional tests of instantiated design
  • Animation of state machines and track layout
  • Scenario export for Hardware In the Loop target validation tests
  • Test documentation export

Code generation

  • Dedicated plugins can take into account any vital execution platform code requirements
  • Code generation


Graphical integrated framework

  • Generic design based on state machine diagrams for functional and vital requirements
  • Counterexample animation over the instantiated diagrams
  • Visualisation of simulation traces
  • Model and test documentation export

Formally aided design

  • Design issue identification
  • Counterexample interpretation
  • Formal proof over the instantiated design
  • EN50128 T2/T3 justifiable


  • Data import plugin to allow specific data formats
  • Code generation plugin to take into account any vital execution platform code requirements

Contact us