Tutorial Unit Plugin With Rodin

Revision as of 13:37, 7 January 2013 by Sebastian Krings (talk | contribs) (Created page with 'Category:Tutorial Category:User Manual This tutorial describes, how ProB's integrated plugin for unit analysis can be used with Event-B machines from inside the Rodin p…')
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)


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.