- About
- Innovations
- Divisions
- Compiler Technology Department
- Computer Systems Department
- Information Systems Department
- Software Engineering Department
- System integration and multi-disciplinary collaborative environments
- System Programming Department
- Theoretical Computer Science Department
- Academic council
- Dissertation council
- Verification Center of the Operating System Linux
- Center of competence in parallel and distributed computing
- Education
- Editions
- News
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
All publications during 2014
All publications