IUML-B Modelling a control system

This page is under development. Later it will be compiled into an illustrated guide using a running example developed in UML-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 aim to use visual animations of the system to validate with stakeholders the controller and the assumptions we make about the environment.

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 (in order to discharge proof obligations) 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.