Ivannikov Institute for System Programming of the RAS

Using Rodin for development and verification of Event-B models.


Ilya Shchepetkov


Modeling of complex systems is often required during phases of design and analysis. Event-B is a formal method for system-level modeling and analysis. The paper presents our experience in using the Rodin platform which provides an environment for development, analysis and verification of Event-B models.

Full text of the paper in pdf (in Russian)


formal verification, Event-B, OS security model


Proceedings of the 11th conference for free software developers, pages 50-52.

Research Group

Software Engineering

All publications during 2014 All publications