Difference between pages "D32 Mathematical Extensions" and "Event-B Language"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
m (→‎Available Documentation: Added references to mathextn and MathExtnSummary on eprints)
 
imported>WikiSysop
 
Line 1: Line 1:
=== Overview ===
+
== Book: Modelling in Event-B: System and Software Engineering by Jean-Raymond Abrial ==
 +
More information about the book is at Cambridge University Press [http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569 website]
 +
=== Sample Chapters of the books ===
 +
This is available at event-b.org [http://www.event-b.org/abook.html]
 +
=== 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]
  
Mathematical extensions have been co-developed by Systerel (for the Core Rodin Platform) and Southampton (for the Theory plug-in). The main purpose of this new feature was to provide the Rodin user with a way to extend the standard Event-B mathematical language, by defining his own mathematical operators, basic predicates and algebraic types. Along with these additional notations, the user can also define new proof rules (prover extensions).
+
== Event-B Language Documentation ==
  
A theory is a file that gathers of new algebraic types, new operators/predicates and new proof rules. It is developed in the Rodin workspace. When it is complete, the user makes it available to his models (this action is called the deployment of a theory). He can then start using his own operators, datatypes and proof rules for the development of his models.
+
[[Event-B Modelling Language]]
  
=== Motivations ===
+
[[Event-B Mathematical Language]]
  
Main reasons for implementing mathematical extensions are:
+
[http://wiki.event-b.org/images/EventB-Summary.pdf Concise Summary of the Event B mathematical toolkit] by Ken Robinson
* increased readability (<math>a \; \operatorname{OR} \; b</math> rather than <math>\operatorname{bool}(a=TRUE \or b=TRUE)</math>)
 
* polymorphism (<math>l \in List(S \cprod T)</math>)
 
* decreased proving effort, thanks to extension specific proof rules instead of general purpose ones
 
  
=== Choices / Decisions ===
+
[[Well-definedness in Event-B]]
  
On the Core Rodin Platform side, implementing mathematical extensions required to make some parts of the code extensible, that were not designed to be so, namely the lexer and the parser. We were using tools that automatically generated them from a fixed grammar description, so we had to change to other technologies. A [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser study] has been made on available technologies. The Pratt algorithm was selected for its adequation with the purpose and it did not have the drawbacks of other technologies:
+
==Modelling Tips==
* foreign language integration
 
* overhead due to over generality
 
  
After a mocking up phase to verify feasibility, the Pratt algorithm has been confirmed as the chosen option and implemented in the Rodin Platform.
+
[[Structured_Types]]
  
Besides, we wanted to set up a way to publish and share theories for Rodin users, in order to constitute a database of pre-built theories for everyone to use and contribute. This has been realised by adding a new tracker on SourceForge site ([http://sourceforge.net/tracker/?group_id=108850&atid=1558661]).
+
[[Category:User documentation]]
 +
[[Category:Event-B]]
  
=== Available Documentation ===
+
== Proving Tips ==
  
{{TODO|add pdf mathextn from BSCW}}
+
== Miscellaneous ==
 
+
* 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].
* Requirements.
 
* Pre-studies (states of the art, proposals, discussions).
 
** [http://deploy-eprints.ecs.soton.ac.uk/216/]
 
** [http://deploy-eprints.ecs.soton.ac.uk/251/]
 
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser#Design_Alternatives]
 
* Technical details (specifications).
 
** [http://wiki.event-b.org/index.php/Mathematical_Extensions]
 
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Lexer]
 
** [http://wiki.event-b.org/index.php/Constrained_Dynamic_Parser]
 
** [http://wiki.event-b.org/index.php/Theory_Plug-in]
 
* Teaching materials (tutorials).
 
* User's guides.  
 
** [http://wiki.event-b.org/images/Theory_UM.pdf]
 
 
 
=== Planning ===
 
This paragraph shall give a timeline and current status (as of 28 Jan 2011).
 
 
 
{{TODO|What will remain to do after Rodin 2.1 ?}}
 
 
 
[[Category:D32 Deliverable]]
 

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 in Event-B

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.