Yoann Guyot, Renaud De Landtsheer, Christophe Ponsard, Building Event-B Interlocking Theories : Lessons Learned using the Theory Plug-in, 6th Rodin User and Developer Workshop, Linz, Austria, 23-24 May, 2016 (accepted)
This talk presents our experience and discusses a number of open questions on the use of the Theory plug-in in the context of a work-in-progress aiming at defining a set of interlocking theories ready to be used by signalling engineers. These theories are made of train-specific constructs with a set of theorems and proof rules. They form a domain specific language (DSL) for modelling interlocking systems that has a fully formal semantics enabling to carry out verification activities but also to perform animation and to generate interlocking systems form the model based on a number of standard Rodin plug-ins.