Tutorial Unit Plugin With Rodin

This tutorial describes, how ProB's integrated plugin for unit analysis can be used with Event-B machines from inside the Rodin platform. This includes

1. Annotating variables with their physical unit,
2. Infer the unit of variables without an annotation,
3. Detect incorrect usage of units, like addition of differently annotated variables.

Both the plugin itself and the bridge to Rodin are a work in progress. Preliminary support is available in the nightly builds of ProB for Rodin and will be merged in the regular releases in the future.

We assume that you have a general understanding of Event-B and the usage of ProB / Rodin.

Installing Physical Units Support for ProB for Rodin

You can follow the First Steps Instructions or the Screencast to install ProB for Rodin.