- 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
Using Rodin for development and verification of Event-B models.
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.