Simple Event-B Train Model for ProB
Abstract
This model accompanies the chapter "ProB for Validation and Verification of B and Event-B". It models a very simple train control system with two trains and contains a safety invariant (inv3) asserting the absence of collisions.
Fields of Study & Subjects
Formal Methods in Verification
Logic
programming
and type systems
Petri Nets in System Modeling
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 4 March 2026
- Language
- EN
- Document type
- Dataset