a Lean4 framework for the modeling and refinement of stateful systems

Convert Event-B machines and contexts (.bum/.buc) to CamilleX plain-text models

Collection of various Event-B models

Open tool platform for the cost effective rigorous development of dependable complex software systems services. This platform is based on the Event-B formal method and provides natural support for refinement and mathematical proof.

A Rust toolchain for Event-B: parser, static checker, CLI and Language Server (LSP) with Rodin round-tripping

CamilleX extension for Rodin platform

Public part of the Event-B specification of the HIMACF model (formerly MROSL DP-model) — role-based access control for OS security

Rodin Platform Bundles that include features developed by our group

A formal specification written in Event-B notation that formally specifies the behaviour of a multi-lift elevator system.

Formal model and verification of a multi-cabin elevator system in Event-B/Rodin, with additional static verification in Ada/SPARK (not in repo), following a requirement specification.

Code generation project of C code from Event-B formal models. Including C metamodel files, C XText files, and Event-B to C translation rules

Adaptation of the EMF translator for Event-B and Rodin

Homebrew tap for the Event-B / B-method ecosystem — Rodin, Atelier B, ProB2-UI, EventBTool

(READ ONLY MIRROR) The Camille Editor for Rodin

Uses lisb to transform an Event-B machine to a B machine. Very experimental.

CODA Component Diagrams

Given a graph grammar defined in AGG (.ggx) using a type graph, converts the file to a new one, usable in Rodin, containing the same definition.

CODA Utilities

Event-B model for University Programme Management System