Interlocking formal design solution
Interlocking systems design and validation require managing both safety and efficiency.
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
- Model a generic design using an OO paradigm focused on class and state machine diagrams
- Deploy the design over imported configuration data
- Formally assess th safety of the instantiated design
- Validate the design with host simulation
- Generate code and certify it
- Replay the validation with the hardware in the loop
Features
Design
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
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
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
Benefits
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
Adaptability
- Data import plugin to allow specific data formats
- Code generation plugin to take into account any vital execution platform code requirements