IUML-B Modelling a control system - Revision history

Colin: remove i

2020-09-30T22:08:33Z

remove i

← Older revision		Revision as of 22:08, 30 September 2020
Line 1:		Line 1:

	This page is under development. Later it will be compiled into an illustrated guide using a running example developed in ~~iUML~~-B.		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.		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.

imported>Colin at 17:09, 26 June 2015

2015-06-26T17:09:10Z

← Older revision		Revision as of 17:09, 26 June 2015
Line 26:		Line 26:
	11. where there are multiple instances of similar I/O channels, as iUML-B Classes with attributes (of type BOOL, NAT, enumerated set).		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.		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.		13. As the model is developed, we add invariants to the machine to give the equivalence between controller states and controller outputs.

imported>Colin at 17:06, 26 June 2015

2015-06-26T17:06:36Z

← Older revision		Revision as of 17:06, 26 June 2015
Line 1:		Line 1:

	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 is under development. Later it will 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~~.		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.		1. In order to prove system wide properties we need to model the system, not just the controller.

imported>Colin at 16:22, 26 June 2015

2015-06-26T16:22:06Z

← Older revision		Revision as of 16:22, 26 June 2015
Line 1:		Line 1:

			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.		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.

	~~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. In order to prove system wide properties we need to model the system, not just the controller.


	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.		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.		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.		4. Our first abstract models will be small abstract statemachines just enough to capture the most important safety properties of the system.
Line 16:		Line 14:
	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.		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. 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.

	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.		13. As the model is developed, we add invariants to the machine to give the equivalence between controller states and controller outputs.

	7. We build up the ~~environment model with many state~~-~~machines, generally one per physical component in~~ the ~~enviroment~~.		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.

	8.		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.

imported>Colin: Created page with " 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..."

2015-06-26T15:10:58Z

Created page with " 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..."

New page

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.