atelier-b
- Ebuilds: 1, Testing: 24.04.2 Description:
Atelier B Community Edition is an IDE by ClearSy for the B
method: type checking, proof obligation generation, automatic
and interactive provers, and code generation from B models.
Homepage:https://www.atelierb.eu/ License: Atelier-B-Community
evbt
- Ebuilds: 1, Testing: 1.5.0 Description:
EventBTool (evbt) works with Event-B models created in the
Rodin Platform: it generates documentation (TeX, HTML) and
translates models into executable code.
Homepage:https://codeberg.org/viklauverk/EventBTool License: AGPL-3+
eventb-animate
- Ebuilds: 1, Testing: 5.0 Description:
eventb-animate animates Event-B models with the ProB model
checker without requiring a Rodin Platform installation:
random animation, invariant checking, and trace save/replay.
Homepage:https://github.com/eventb-rossi/eventb-animate License: Apache-2.0
eventb-checker
- Ebuilds: 1, Testing: 1.7 Description:
eventb-checker validates Event-B models without requiring a
Rodin Platform installation. It bundles the Rodin AST libraries
and checks machines and contexts for well-formedness errors.
Homepage:https://github.com/eventb-rossi/eventb-checker License: MIT
eventb-to-txt
- Ebuilds: 1, Testing: 1.7 Description:
eventb-to-txt converts Event-B models created in the Rodin
Platform (.bum and .buc files) to a plain-text CamilleX-like
format. Compatible with Rodin 3.0 and later models.
Homepage:https://github.com/eventb-rossi/eventb-to-txt License: MIT
prob-bin
- Ebuilds: 1, Testing: 1.15.1 Description:
ProB is an animator, constraint solver and model checker for the
B method. It supports classical B, Event-B, CSP-M, TLA+ and Z,
and allows the animation and automated/guided model checking of
specifications, including invariant and deadlock checking. This
package installs the prebuilt Tcl/Tk graphical interface (prob)
and the command-line tool (probcli).
Homepage:https://prob.hhu.de/ License: EPL-1.0
prob2-ui
- Ebuilds: 1, Testing: 1.3.1 Description:
ProB2-UI is a modern JavaFX-based user interface for the ProB
animator, constraint solver and model checker. It supports the
B method, Event-B, CSP-M, TLA+ and Z, offering interactive
animation, model checking, LTL/CTL verification, trace
recording and replay, and visualisation.
Homepage:https://prob.hhu.de/ License: EPL-2.0
rodin
- Ebuilds: 2, Testing: 3.10.0_rc2 Description:
The Rodin Platform is an Eclipse-based IDE for Event-B that
provides effective support for refinement and mathematical
proof. Event-B is a formal method for system-level modelling
and analysis.
Homepage:https://www.event-b.org/ License: EPL-1.0 EPL-2.0
rossi
- Ebuilds: 1, Testing: 0.1.0 Description:
Rossi is a Rust toolchain for Event-B providing a parser, a static
checker, a command-line interface, and a language server. It validates
Event-B models, converts between Event-B text and Rodin archives,
reformats models, and powers editor integration over the Language
Server Protocol.
Homepage:https://github.com/eventb-rossi/rossi License: || ( Apache-2.0 MIT )
Apache-2.0 Apache-2.0-with-LLVM-exceptions MIT Unicode-3.0 ZLIB
BZIP2
|| ( CC0-1.0 MIT-0 )
tlc4b
- Ebuilds: 1, Testing: 1.2.3 Description:
TLC4B model-checks classical B specifications by translating
them to TLA+ and running the TLC model checker: invariant and
assertion checking, deadlock detection, and counter-example
traces mapped back to B.
Homepage:https://github.com/hhu-stups/tlc4b License: EPL-1.0