Difference between pages "IUML-B Modelling a control system" and "Template:Dev News"

From Event-B
(Difference between pages)
Jump to navigationJump to search
m (remove i)
 
 
Line 1: Line 1:
−
 
+
<noinclude>
−
This page is under development. Later it will be compiled into an illustrated guide using a running example developed in UML-B.
+
[http://wiki.event-b.org/index.php?title=Template:Dev_News/Archives&action=edit Edit Archives]
−
 
+
== Displayed as follow on the Main Page ==
−
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.
+
<div style="margin:0;width:50%;border:1px solid #AAAAAA;background:#FFFFFF;">
−
 
+
</noinclude><!--- News to add here below : ==== --->
−
1. In order to prove system wide properties we need to model the system, not just the controller.
+
<div style="font-size:90%;">
−
 
+
{| border="0"
−
2. In order to run animations we need to model both the controller and the environment.
+
|-
−
 
+
|<p style="font-size:35px">Rodin 3.6 is out&nbsp;&nbsp;&nbsp;</p>
−
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.
+
||<p style="font-size:25px">[[Rodin Platform 3.6 Release Notes | +Learn more... ]]</p>
−
 
+
  <p style="font-size:25px">[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.6/ Download now]</p>
−
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.
+
* 17/05/21 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.6/ Release 3.6] of Rodin is now available
−
 
+
* 22/12/20 : [[Theory_Plug-in]] Theory 4.0.1 is now available
−
6. At these early stages the interaction is modelled by direct access to the states of the other components (e.g. in transition guards).
+
* 11/09/20 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.5/ Release 3.5] of Rodin is now available [[Rodin Platform 3.5 Release Notes | +Learn more]]
−
 
+
* 07/03/18 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.4/ Release 3.4] of Rodin is now available [[Rodin Platform 3.4 Release Notes | +Learn more]]
−
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.
+
* 13/04/17 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.3/ Release 3.3] of Rodin is now available [[Rodin Platform 3.3 Release Notes | +Learn more]]
−
 
+
* 22/06/15 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.2/ Release 3.2] of Rodin is now available [[Rodin Platform 3.2 Release Notes | +Learn more]]
−
8. We build up the environment model with many state-machines, generally one per physical component in the environment.  
+
* 17/12/14 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.1/ Release 3.1] of Rodin is now available [[Rodin Platform 3.1 Release Notes | +Learn more]]
−
 
+
* 25/03/14 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.0/ Release 3.0] of Rodin is now available [[Rodin_Platform_3.0_Release_Notes | +Learn more]]
−
9. We gradually replace the unrealistic direct access between controller and physical components with the actual I/O interface of the controller.
+
* 18/10/13 : [[SMT_Solvers_Plug-in]] SMT 1.1 is now available
−
 
+
* 20/06/13 : [https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.8/ Release 2.8] of Rodin is now available [[Rodin_Platform_2.8_Release_Notes | +Learn more]]
−
10. We model the I/O interface either as variables (of type BOOL, NAT, enumerated set) directly in the machine, or
+
* 03/06/13 : [[SMT_Solvers_Plug-in]] SMT 1.0 is now available
−
 
+
* 06/11/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.7/ Release 2.7] of Rodin is now available
−
11. where there are multiple instances of similar I/O channels, as iUML-B Classes with attributes (of type BOOL, NAT, enumerated set).
+
* 03/08/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.6/ Release 2.6] of Rodin is now available
−
 
+
* 02/05/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.5/ Release 2.5] of Rodin is now available
−
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.  
+
* 03/02/12 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.4/ Release 2.4] of Rodin is now available
−
 
+
* 01/12/11 : [[Rodin_Editor | Rodin Editor]] plug-in v0.6 released for Rodin 2.3
−
13. As the model is developed, we add invariants to the machine to give the equivalence between controller states and controller outputs.
+
* 04/10/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.3/ Release 2.3] of Rodin is now available
−
 
+
* 01/08/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.2.2/ Release 2.2.2] of Rodin is now available
−
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.  
+
* 13/07/11 : [[Rodin_Editor | Rodin Editor]] plug-in released for Rodin 2.2.x
−
 
+
* 01/06/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.2/ Release 2.2] of Rodin is now available
−
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.
+
<!--
 +
* 08/02/11 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.1/ Release 2.1] of Rodin is now available
 +
* 16/11/10 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.0.1/ Release 2.0.1] of Rodin is now available
 +
* 13/10/10 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.0/ Release 2.0] of Rodin is now available
 +
* 08/06/10 : UML-B Statemachine Animation Version 1.0.0 released (for Rodin 1.3)
 +
* 08/06/10 : UML-B Version 1.1.0 released (for Rodin 1.3)
 +
* 03/02/10 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/1.2/ Release 1.2.0] of Rodin is now available
 +
* 29/11/09 : B2Latex 0.5.1 is now available for Rodin 0.9.2 or later
 +
* 20/10/09 : [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/1.1/ Release 1.1.0] of Rodin is now available
 +
* 25/08/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/248437 Implemented new Prover Rules]
 +
* 20/08/09 : [http://cia.vc/stats/project/rodin-b-sharp/.message/24160f New extensible plug-ins] org.rodinp.keyboard and org.eventb.keyboard
 +
* 31/07/09 : UML-B plug-in released for Rodin 1.0.0
 +
* 27/07/09 : Fixed requirement plug-in for rodin 1.0.0
 +
* 01/07/09 : [https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/1.0/ Release 1.0.0] of Rodin is now available ([http://sourceforge.net/project/shownotes.php?release_id=693928 changelog]-->
 +
</div>
 +
<noinclude>
 +
</div>
 +
[[Category:Main page templates]]
 +
</noinclude>

Revision as of 09:14, 17 May 2021

Edit Archives

Displayed as follow on the Main Page

Rodin 3.6 is out   

+Learn more...

Download now

Retrieved from ‘https://wiki.event-b.org/index.php?title=IUML-B_Modelling_a_control_system&oldid=14414’