Difference between revisions of "Event-B Language"

From Event-B
Jump to navigationJump to search
imported>Mathieu
imported>Laurent
 
(33 intermediate revisions by 6 users not shown)
Line 1: Line 1:
 +
== Book: Modeling 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].
 +
 +
The Event-B introduced in Abrial's book in some ways differs from the Event-B implemented by Rodin.
 +
Some of those differences are listed [[How Rodin Deviates from Abrial's Book|here]].
 +
 +
=== Sample Chapters of the Book ===
 +
These are available at [http://www.event-b.org/abook.html event-b.org].
 +
=== 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]
 +
 +
=== Japanese Language ===
 +
 +
[http://www.jfp.co.jp/slp/eventb.htm Japanese translation of Chapter 1-2 of ''Modeling in Event-B''] by JFP, Inc.
 +
 
== Event-B Language Documentation ==
 
== Event-B Language Documentation ==
  
[[Event-B Mathematical Language]]
+
=== [[Event-B Modelling Language]]===
  
[[Event-B Modelling Language]]
+
=== [[Event-B Mathematical Language]] ===
  
[[Category:User Documentation]]
+
=== Draft book by Ken Robinson: [http://wiki.event-b.org/index.php/Image:SM%26D-KAR.pdf System Modelling & Design Using Event-B.] ===
 +
 
 +
=== [[Media:EventB-Summary.pdf|Concise Summary of the Event B mathematical toolkit]] by Ken Robinson ===
 +
 
 +
=== [[Media:EventB-Summary-refcard.pdf|Event B Reference Card]] by Ken Robinson ===
 +
 
 +
==Modelling Tips==
 +
 
 +
[[Structured_Types]]
 +
 
 +
[[Proof Hints]]
 +
 
 +
[[Category:User documentation]]
 
[[Category:Event-B]]
 
[[Category:Event-B]]
 +
 +
== Proving Tips ==
 +
 +
== 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].

Latest revision as of 11:30, 23 January 2014

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

More information about the book is at Cambridge University Press website.

The Event-B introduced in Abrial's book in some ways differs from the Event-B implemented by Rodin. Some of those differences are listed here.

Sample Chapters of the Book

These are available at event-b.org.

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

Japanese Language

Japanese translation of Chapter 1-2 of Modeling in Event-B by JFP, Inc.

Event-B Language Documentation

Event-B Modelling Language

Event-B Mathematical Language

Draft book by Ken Robinson: System Modelling & Design Using Event-B.

Concise Summary of the Event B mathematical toolkit by Ken Robinson

Event B Reference Card by Ken Robinson

Modelling Tips

Structured_Types

Proof Hints

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.