IUML-B Modelling a control system

This page gives some guidelines for developing a control system using iUML-B.

This page is under development. Currently it is just a few notes which will later be compiled into an illustrated guide using a running example.

1. We aim to verify (prove) some safety properties of the controller as well as perform visual animations in order to validate it.

2. In order to run animations we need to model both the controller and the environment.

3. However, the environment model contains assumptions about the possible behaviours of the environment. We also need to test the behaviour of the controller for less well behaved inputs.

4. Our first abstract models will be small abstract statemachines just enough to capture the most important safety properties of the system.

5. The initial refinements introduce the distinction between the controller and physical components of the environment in order to verify that their interaction maintains the safety of the abstract model.

6. At these early stages the interaction is modelled by direct access to the states of the other components in transition guards

6. We aim to build up the controller model via hierarchical nesting as far as possible. Ideally their should only be one statemachine representing the controller.

7. We build up the environment model with many state-machines, generally one per physical component in the enviroment.

8.