Using the Rodin Platform as a Programming Tool

Adrian Turcanu*, Florentin Ipate

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Being the result of several research projects that involved at the same time academic and industrial partners, the Rodin platform is designed to implement and analyse mathematical models of transitional systems based on Event-B language. Several plugins were integrated in the platform including ProB, a model checker that can be used to verify LTL properties or animate the model. In this paper, we introduce a methodology for using the Rodin platform and ProB as a powerful, integrated, programming and analysis environment. Our approach is based on assigning an FSM to an algorithm, then implementing the corresponding Event-B model in Rodin, and finally verifying its correctness and finiteness using the facilities of the platform.

Original languageEnglish
Title of host publicationProceedings of International Conference on Information Technology and Applications. ICITA 2021
EditorsAbrar Ullah, Steve Gill, Álvaro Rocha, Sajid Anwar
Number of pages9
ISBN (Electronic)9789811676185
ISBN (Print)9789811676178
Publication statusPublished - 21 Apr 2022
Event15th International Conference on Information Technology and Applications 2021 - Dubai, United Arab Emirates
Duration: 13 Nov 202114 Nov 2021

Publication series

NameLecture Notes in Networks and Systems
ISSN (Print)2367-3370
ISSN (Electronic)2367-3389


Conference15th International Conference on Information Technology and Applications 2021
Abbreviated titleICITA 2021
Country/TerritoryUnited Arab Emirates


  • Algorithms
  • Event-B language
  • Formal verification
  • FSM
  • Mathematical modelling
  • Model checking
  • Rodin platform

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Signal Processing
  • Computer Networks and Communications


Dive into the research topics of 'Using the Rodin Platform as a Programming Tool'. Together they form a unique fingerprint.

Cite this