IUML-B Modelling a control system

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 developed in iUML-B.

This page gives some guidelines for developing a control system using iUML-B. We aim to verify (i.e. prove) some safety properties of the system, comprising the controller and the environment that it is controlling. We also need to perform visual animations of the system in order to validate the controller and assumptions about the environment with stakeholders.

1. In order to prove system wide properties we need to model the system, not just the controller.

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 (e.g. in transition guards).

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

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

9. We gradually replace the unrealistic direct access between controller and physical components with the actual I/O interface of the controller.

10. We model the I/O interface either as variables (of type BOOL, NAT, enumerated set) directly in the machine, or

11. where there are multiple instances of similar I/O channels, as iUML-B Classes with attributes (of type BOOL, NAT, enumerated set).

12. While developing refinements we add invariants to states about a) states of other components and b) the value of outputs.

13. As the model is developed, we add invariants to the machine to give the equivalence between controller states and controller outputs.

14. We build different versions of environment models a) liberal models that can behave in unexpected ways to test the controllers response to fault scenarios, b) well-behaved models to test the controllers response to normal situations.

15. Note that well-behaved models of the environment (i.e. 14 b) document assumptions about the environment that we rely on for succesful control.