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


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

Authors

Ilya Shchepetkov

Abstract

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)

Keywords

formal verification, Event-B, OS security model

Edition

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

Research Group

Software Engineering

All publications during 2014 All publications