Difference between pages "UML-B" and "IUML-B Modelling a control system"

From Event-B
(Difference between pages)
Jump to navigationJump to search
m (remove some i)
 
m (remove i)
 
Line 1: Line 1:
Return to [[Rodin Plug-ins]]
 
  
UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. [[UML-B]] works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams.  
+
This page is under development. Later it will be compiled into an illustrated guide using a running example developed in UML-B.
  
Our [https://www.uml-b.org UML-B] website contains more information about installing UML-B and getting started, as well as our current research and collaborations.
+
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.
  
UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine.
+
1. In order to prove system wide properties we need to model the system, not just the controller.
  
* [[Image:IUMLB.png]] [[Event-B Statemachines| State-machine diagrams]] a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.
+
2. In order to run animations we need to model both the controller and the environment.
  
* [[Image:IUMLB.png]] [[Event-B Classdiagrams| Class diagrams]] a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets.
+
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.
  
==Lectures==
+
4. Our first abstract models will be small abstract statemachines just enough to capture the most important safety properties of the system.
  
* [[Media:iUML-BClassDiagramsLecture.pdf | UML-B Class-diagrams Lecture]] : Lecture slides on the use of UML-B Class-diagrams
+
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.
  
* [[Media:iUML-BStatemachinesLecture.pdf | UML-B State-machines Lecture]] : Lecture slides on the use of UML-B State-machines.
+
6. At these early stages the interaction is modelled by direct access to the states of the other components (e.g. in transition guards).
  
==Tutorials==
+
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.
  
* [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of iUML-B Class-diagrams.
+
8. We build up the environment model with many state-machines, generally one per physical component in the environment.  
  
* [[iUML-B State-machines Tutorial]] : A tutorial on the use of iUML-B State-machines.
+
9. We gradually replace the unrealistic direct access between controller and physical components with the actual I/O interface of the controller.
  
==Guidelines==
+
10. We model the I/O interface either as variables (of type BOOL, NAT, enumerated set) directly in the machine, or
  
* [[iUML-B Modelling a control system]] : Some guidelines on modelling styles for a control system
+
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.
  
[[Category:User documentation]]
+
13. As the model is developed, we add invariants to the machine to give the equivalence between controller states and controller outputs.
[[Category:UML-B]]
+
 
[[Category:Plugin]]
+
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.

Latest revision as of 22:08, 30 September 2020

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.