Difference between pages "Element Hierarchy Extension Point & Library" and "Event-B Examples"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
m
 
imported>Son
 
Line 1: Line 1:
−
The UI in Rodin 2.x contains an extension point <tt>org.eventb.ui.editorItems</tt> that groups the both following information:
+
{{TOCright}}
−
*the definition of elements and attributes and their hierarchy, and the way they are created
+
This page is for listing available example Event-B/Rodin projects.
−
*the information needed to correctly display and edit these elements in the various editors and UI components
 
  
−
It appears obvious that the first information should be defined from an extension that belongs to the Database.
 
−
To fullfil the above statement, the current extension point <tt>org.eventb.ui.editorItems</tt> should be split in two.
 
−
The existing extension point was also heterogenous. Indeed, whereas the element relationships were concerning element types, the attribute relationship were concerning element types and references to UI defined attributes (referring to core attributes).<br>
 
−
There is no need for such an indirection.
 
  
−
----
+
== Year 2009 ==
−
The proposal should concern :
 
−
A - Relationship declaration (new extension point)
 
−
B - API to test these relations and traverse them
 
−
C - Enforcement of the authorized relations when modifying the DB
 
−
D- What about the compatibilty with the file upgrade mechanism?
 
−
----
 
  
−
= Some identified difficulties =
+
=== [http://deploy-eprints.ecs.soton.ac.uk/82/ Development of a Network Topology Discovery Algorithm]===
 +
By ''Hoang, Thai Son and Basin, David and Kuruma, Hironobu and Abrial, Jean-Raymond''.
  
−
== Initialization of elements from non UI components ==
+
This paper and this Rodin development is another version of the [[#Link State Routing Development]] presented in 2008.
  
−
The following ElementDescRegistry method, shows the dependency between an element creation and the initialization of its attributes with default values.
+
== Year 2008 ==
 +
=== [http://deploy-eprints.ecs.soton.ac.uk/31/ Link State Routing Development]===
 +
By ''Hoang, Thai Son and Basin, David and Kuruma, Hironobu and Abrial, Jean-Raymond''.
  
−
        public <T extends IInternalElement> T createElement(
+
We present a formal development in Event-B of a distributed topology discovery algorithm. Distributed topology discovery is at the core several routing algorithms and is the problem of each node in a network discovering and maintaining information on the network topology. One of the key challenges in developing this algorithm is specifying the problem itself.We provide a specification that includes both safety properties, formalizing invariants that should hold in all system states, and liveness properties that characterize when the system reaches stable states. We specify these by appropriately combining invariants, event refinement, and proofs of event convergence and deadlock freedom. The combination of these features is novel and should be useful for formalizing and developing other kinds of semi-reactive systems, which are systems that react to, but do not modify, their environment.
−
final IInternalElement root, IInternalElement parent,
 
−
final IInternalElementType<T> type, final IInternalElement sibling)
 
−
throws RodinDBException {
 
−
final T newElement = parent.createChild(type, sibling, null);
 
−
final IAttributeDesc[] attrDesc = getAttributes(type);
 
−
for (IAttributeDesc desc : attrDesc) {
 
−
desc.getManipulation().setDefaultValue(newElement, null);    // <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
 
−
}
 
−
return newElement;
 
−
}
 
  
−
The protocol shall be changed to take into account this initialization outside from the graphical manipulation.
+
=== [http://deploy-eprints.ecs.soton.ac.uk/22/ Modelling and proof of a Tree-structured File System] ===
−
Doing the initialization at org.eventb.core level is possible by registering a special "attribute initializer". <br>
+
By ''Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.
−
WARNING : Only "choice" attributes can be marked as mandatory ({{ident|required}} attribute of the extension). Can't it be available for all kind of attributes?
 
  
−
== Correspondence between UI manipulation and "core" elements ==
+
We present a verified model of a tree-structured file system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities affecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a file system, we begin with an abstract model of a file system and subsequently refine it by adding more details through refinement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.
−
If some element or attribute relationship is declared at the database level, but there is no corresponding {{ident|editorItem}} for it, it will be ignored by the UI. This is similar to the previous situation where some elements or attributes could be present in the database but not in the user interface hierarchy.
 
  
−
== Operation on elements shall be enforced ==
+
=== [http://deploy-eprints.ecs.soton.ac.uk/56/ Deliverable D8 D10.1 "Teaching Materials"] ===
−
+
By ''Abrial, Jean-Raymond and Hoang, Thai Son and Schmalz, Matthias''.
−
        private <T extends IInternalElement> OperationCreateElement getCreateElement(
 
−
IInternalElement parent, IInternalElementType<T> type,
 
−
IInternalElement sibling, IAttributeValue[] values) {
 
−
OperationCreateElement op = new OperationCreateElement(
 
−
createDefaultElement(parent, type, sibling));
 
−
op.addSubCommande(new ChangeAttribute(values));
 
−
return op;
 
−
}
 
  
−
''The Operation model similar to a kind of transaction mechanism, should be made available from the DB layer.''<br>
+
==Year 2007==
−
''The relations when using such layer shall be enforced and any invalid operation could be rejected.''
+
=== [http://deploy-eprints.ecs.soton.ac.uk/9/ Redevelopment of an Industrial Case Study Using Event-B and Rodin]===
 +
From ''Rezazadeh, Abdolbaghi and Butler, Michael and Evans, Neil''.
  
−
= Proposal =
+
CDIS is a commercial air traffic information system that was developed using formal methods 15 years ago by Praxis, and it is still in operation today. This system is an example of an industrial scale system that has been developed using formal methods. In particular, the functional requirements of the system were specified using VVSL -- a variant of VDM. A subset of the original specification has been chosen to be reconstructed on the Rodin platform based on the new Event-B formalism. The goal of our reconstruction was to overcome three key difficulties of the original formalisation, namely the difficulty of comprehending the original specification, the lack of any mechanical proof of the consistency of the specification and the difficulty of dealing with distribution and atomicity refinement. In this paper we elucidate how a new formal notation and tool can help to overcome these difficulties.
  
−
== Hierarchy between elements ==
+
[[Category:Examples]]
−
 
 
−
The part concerning element definition and hierarchy will go to a dedicated extension point in the database.
 
−
 
 
−
=== A - hierarchy definition ===
 
−
 
 
−
Here is the definition of the new extension point : org.rodinp.core.itemRelations which describes the possible children and attributes of internal elements.
 
−
 
 
−
Configuration Markup:
 
−
<!ELEMENT extension (relationship+)>
 
−
<!ATTLIST extension
 
−
point CDATA #REQUIRED
 
−
id    CDATA #IMPLIED
 
−
name  CDATA #IMPLIED
 
−
>
 
−
 
−
<!ELEMENT relationship ((childType | attributeType)+)>
 
−
<!ATTLIST elementRelationship
 
−
parentTypeId CDATA #REQUIRED
 
−
>
 
−
parentTypeId - Element type of the parent, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
 
−
 
−
<!ELEMENT childType EMPTY>
 
−
<!ATTLIST childType
 
−
typeId                CDATA #REQUIRED
 
−
>
 
−
typeId - Element type of the child, must be the unique ID of a Rodin internal element type (see extension point org.rodinp.core.internalElementTypes).
 
−
 
−
<!ELEMENT attributeType EMPTY>
 
−
<!ATTLIST attributeType
 
−
typeId CDATA #REQUIRED
 
−
>
 
−
attributeTypeId - Id of the Rodin attribute type to which this description applies (see extension point org.rodinp.core.attributeTypes).
 
−
 
−
The use of such extension point is obvious in org.eventb.core plug-in, as it would complement the extensions of org.rodinp.core.attributeTypes and org.rodinp.core.internalElementTypes.
 
−
 
 
−
=== B - API to declare and test the element/attribute relations and traverse them ===
 
−
 
 
−
The API of the Rodin database is extended as follows:
 
−
 
 
−
* interface IInternalElementType is extended with methods
 
−
 
 
−
  IInternalElementType<?>[] getParentTypes();
 
−
  IInternalElementType<?>[] getChildTypes();
 
−
  IAttributeType[] getAttributeTypes();
 
−
 
 
−
  boolean canParent(IInternalElementType<?> childType);
 
−
  boolean isElementOf(IAttributeType attrType);
 
−
 
 
−
* interface IAttributeType is extended with methods
 
−
 
 
−
  IInternalElementType<?>[] getElementTypes();
 
−
 
 
−
  boolean isAttributeOf(IInternalElementType<?> elementType);
 
−
 
 
−
This list might be later extended with new methods such as
 
−
{{ident|isAncestorOf}} if this proves useful.
 
−
 
 
−
=== C - Data model operations (enforced) ===
 
−
The ElementManipulationFacade, support for modifications over the Database, should be provided by the Event-B Core plug-in.<br>
 
−
The IAttributeManipulation interface should be also provided by the Event-B Core plug-in as it concerns the manipulation done on the attribute in the DB.
 
−
 
 
−
The information about the rendering of an element or an attribute, should not be deduced from the attribute itself (e.g. choiceAttribute vs. toggleAttribute vs. textAttribute), it should be given in the UI.
 
−
 
 
−
It seems that the ElementManipulationFacade can be used as protocol, but hiercharchy between elements and elements, or between elements and attributes shall be enforced.
 
−
''Proposition : add Exceptions to methods of the protocol.''
 
−
 
 
−
== UI related information ==
 
−
The part concerning how to display elements and UI related info will stay in the editorItems extension point and shall point to an element definition and hierachy.<br>
 
−
Relationships will disappear from the editorItems extension point.
 
−
 
 
−
The interfaces are refactored to become the following :
 
−
 
 
−
''NB. IITemDesc disappears as it is cumbersome to provide such interface for a sole method getPrefix(). ''
 
−
 
 
−
public interface IUIElementDesc extends IItemDesc {
 
−
 
−
        public String getPrefix();
 
−
 
−
public String getChildrenSuffix();
 
−
 
−
public IImageProvider getImageProvider();
 
−
 
−
public IAttributeDesc atColumn(int i);
 
−
 
−
public int getDefaultColumn();
 
−
 
−
public boolean isSelectable(int i);
 
−
 
−
public String getAutoNamePrefix();
 
−
 
−
public IElementPrettyPrinter getPrettyPrinter();
 
−
 
−
}
 
−
 
 
−
public interface IUIAttributeDesc extends IItemDesc {
 
−
 
−
        public String getPrefix();
 
−
 
−
public String getSuffix();
 
−
 
−
public IEditComposite createWidget();
 
−
 
−
public boolean isHorizontalExpand();
 
−
 
−
}
 
−
 
 
−
 
 
−
=== D - Compatibility with the upgrade mechanism ===
 
−
 
 
−
Things start with the org.rodinp.core.conversion extension point.<br>
 
−
The modifications are done in XPATH  there is no incompatibility introduced here.
 
−
 
 
−
[[Category:Design_proposal]]
 

Revision as of 15:34, 11 February 2009

This page is for listing available example Event-B/Rodin projects.


Year 2009

Development of a Network Topology Discovery Algorithm

By Hoang, Thai Son and Basin, David and Kuruma, Hironobu and Abrial, Jean-Raymond.

This paper and this Rodin development is another version of the #Link State Routing Development presented in 2008.

Year 2008

Link State Routing Development

By Hoang, Thai Son and Basin, David and Kuruma, Hironobu and Abrial, Jean-Raymond.

We present a formal development in Event-B of a distributed topology discovery algorithm. Distributed topology discovery is at the core several routing algorithms and is the problem of each node in a network discovering and maintaining information on the network topology. One of the key challenges in developing this algorithm is specifying the problem itself.We provide a specification that includes both safety properties, formalizing invariants that should hold in all system states, and liveness properties that characterize when the system reaches stable states. We specify these by appropriately combining invariants, event refinement, and proofs of event convergence and deadlock freedom. The combination of these features is novel and should be useful for formalizing and developing other kinds of semi-reactive systems, which are systems that react to, but do not modify, their environment.

Modelling and proof of a Tree-structured File System

By Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond.

We present a verified model of a tree-structured file system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities affecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a file system, we begin with an abstract model of a file system and subsequently refine it by adding more details through refinement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.

Deliverable D8 D10.1 "Teaching Materials"

By Abrial, Jean-Raymond and Hoang, Thai Son and Schmalz, Matthias.

Year 2007

Redevelopment of an Industrial Case Study Using Event-B and Rodin

From Rezazadeh, Abdolbaghi and Butler, Michael and Evans, Neil.

CDIS is a commercial air traffic information system that was developed using formal methods 15 years ago by Praxis, and it is still in operation today. This system is an example of an industrial scale system that has been developed using formal methods. In particular, the functional requirements of the system were specified using VVSL -- a variant of VDM. A subset of the original specification has been chosen to be reconstructed on the Rodin platform based on the new Event-B formalism. The goal of our reconstruction was to overcome three key difficulties of the original formalisation, namely the difficulty of comprehending the original specification, the lack of any mechanical proof of the consistency of the specification and the difficulty of dealing with distribution and atomicity refinement. In this paper we elucidate how a new formal notation and tool can help to overcome these difficulties.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Element_Hierarchy_Extension_Point_%26_Library&oldid=4071’