Difference between pages "Event-B Classdiagrams" and "Event-B Language"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
imported>WikiSysop
 
Line 1: Line 1:
−
''this page is under construction''
+
== Book: Modelling in Event-B: System and Software Engineering by Jean-Raymond Abrial ==
−
[[Image:IUMLB_big.png|frame|left]]
+
More information about the book is at Cambridge University Press [http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569 website]
−
{{TOCright}}
+
=== Sample Chapters of the books ===
−
==Introduction==
+
This is available at event-b.org [http://www.event-b.org/abook.html]
−
In iUML-B, Class diagrams are used to define and visualize entity-relationship data models. They can be added to Event-B Machines and Event-B Contexts and visualize given sets , constants and variables. Diagram elements elaborate pre-existing user data in order to visualize it. The diagram defines type, sub-type and further constraint information for the data by generating invariants or axioms.
+
=== Slides and Rodin Platform archives of the developments corresponding to chapters of the books ===
 +
* Chapter 1: [http://deploy-eprints.ecs.soton.ac.uk/111/ Introduction]
 +
* Chapter 2: [http://deploy-eprints.ecs.soton.ac.uk/112/ Controlling Cars on a Bridge]
 +
* Chapter 3: [http://deploy-eprints.ecs.soton.ac.uk/113/ A Mechanical Press Controller]
 +
* Chapter 4: [http://deploy-eprints.ecs.soton.ac.uk/114/ File Transfer Protocol]
 +
* Chapter 6: [http://deploy-eprints.ecs.soton.ac.uk/115/ The Bounded Re-transmission Protocol]
 +
* Chapter 7: [http://deploy-eprints.ecs.soton.ac.uk/116/ Concurrent Program Development]
 +
* Chapter 8: [http://deploy-eprints.ecs.soton.ac.uk/117/ Electronic Circuits Development]
 +
* Chapter 10: [http://deploy-eprints.ecs.soton.ac.uk/118/ Leader Election on a Ring-shaped Network]
 +
* Chapter 11: [http://deploy-eprints.ecs.soton.ac.uk/119/ Synchronizing Processes on a Tree Network]
 +
* Chapter 12: [http://deploy-eprints.ecs.soton.ac.uk/120/ Routing Algorithm for Mobile Agent]
 +
* Chapter 13: [http://deploy-eprints.ecs.soton.ac.uk/121/ The Leader Election Protocol (IEEE1394)]
 +
* Chapter 15: [http://deploy-eprints.ecs.soton.ac.uk/122/ Sequential Program Development]
 +
* Chapter 16: [http://deploy-eprints.ecs.soton.ac.uk/123/ Location Access Controller]
 +
* Chapter 17: [http://deploy-eprints.ecs.soton.ac.uk/124/ Train System]
  
−
==Principles of Operation==
+
== Event-B Language Documentation ==
  
−
Classes, Attributes and Associations are all model elements that represent data. They can be linked to existing Event-B data elements: Variables, Constants or (for Classes only) Carrier Sets. This relationship is called ''Elaborates'' because the diagram element elaborates properties of the data item.
+
[[Event-B Modelling Language]]
  
−
Any data element within scope, locally within the same machine or context, or via sees and extends, can be elaborated. As a short cut, a button is provided to create a new data item and link to it in one step.
+
[[Event-B Mathematical Language]]
  
−
Class diagrams can be added to Machines or Contexts, but note that some features are not available when in a Context (e.g. only constants and sets are within scope to link to and methods cannot be used in classes).
+
[http://wiki.event-b.org/images/EventB-Summary.pdf Concise Summary of the Event B mathematical toolkit] by Ken Robinson
  
−
Methods can be placed inside Classes and link (elaborate) one or more events in the containing Machine. This means that the elaborated events are given a paramter representing the class instance (similar to 'this' or 'self' in programming languages). When in variable classes (i.e. a class that elaborates a variable) methods may be constructors or destructors.
+
[[Well-definedness]]
  
−
==Main Data Elements of a Class Diagram==
+
==Modelling Tips==
−
The main data elements of a class diagram are ''class'', ''association'' and ''attribute''. These elements all visualize an Event-B data item (set constant or variable) in the Event-B model. Only a class can visualize a set. The class diagram also visualizes the type and subtype of the data item as follows.
 
−
===Class===
 
−
A Class visualizes a data item that is a set or subset.
 
−
a) If the class diagram is in a Context and the class has no generalization relationships, and its
 
−
===Association===
 
−
===Atttribute===
 
  
−
==Elaboration and Generation==
+
[[Structured_Types]]
−
tbd
 
  
−
==Scope==
+
[[Category:User documentation]]
−
Elements of the class diagram can define data in the containing Event-B component and can visualize data in any Event-B component that is visible to the containing Event-B component (including itself). Hence a class diagram in a context may define/visualize sets and constants in the containing context and visualize sets and constants in any context which is extended (closure) by the containing context.  A class diagram in a machine may define/visualize variables in the containing machine, visualize variables in any machine it refines (closure) and visualize sets and constants in any context that is seen by the machine or any Context that is extended by a context that is seen by the machine.
+
[[Category:Event-B]]
  
−
==Secondary information==
+
== Proving Tips ==
−
Colour is used to indicate whether a diagram element has been linked to data. Icons are used to indicate the kind (set, constant or variable) of elaborated data.
 
  
−
==Example==
+
== Miscellaneous ==
−
For example when a class diagram is first drawn and has not been linked to data it looks like this:
+
* Jean-Raymond Abrial, "Faultless Systems: Yes We Can!," Computer, vol. 42, no. 9, pp. 30-36, Sept. 2009, [http://doi.ieeecomputersociety.org/10.1109/MC.2009.283 doi:10.1109/MC.2009.283].
−
 
 
−
[[File:Cd1_unlinked.png]]
 
−
 
 
−
Generating this diagram produces no output to the Event-B.
 
−
The diagram elements must first be linked to data using the '''Link Data''' or '''Create & Link''' buttons in the properties sheet.
 
−
The followng screenshot shows the association being linked to a variable ''b'' that already exists in the machine.
 
−
 
 
−
[[File:LinkData.png|800px]]
 
−
 
 
−
The following screenshot shows the class A being used to create and link to a carrier set in the seen context X0. Note that the carrier set is created in X0 immediately. It is not necessary to generate.
 
−
 
 
−
[[File:CreatLink.png|800px]]
 
−
 
 
−
==Class Diagrams in Contexts==
 
−
subtype
 
−
 
 
−
==Class Diagrams in Machines==
 

Revision as of 16:23, 18 December 2009

Book: Modelling in Event-B: System and Software Engineering by Jean-Raymond Abrial

More information about the book is at Cambridge University Press website

Sample Chapters of the books

This is available at event-b.org [1]

Slides and Rodin Platform archives of the developments corresponding to chapters of the books

Event-B Language Documentation

Event-B Modelling Language

Event-B Mathematical Language

Concise Summary of the Event B mathematical toolkit by Ken Robinson

Well-definedness

Modelling Tips

Structured_Types

Proving Tips

Miscellaneous

  • Jean-Raymond Abrial, "Faultless Systems: Yes We Can!," Computer, vol. 42, no. 9, pp. 30-36, Sept. 2009, doi:10.1109/MC.2009.283.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_Classdiagrams&oldid=4145’