Event-B Language: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Mathieu
m Robot: Changing Category:User Documentation
imported>Laurent
 
(31 intermediate revisions by 5 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 Modelling Language]]  
=== [[Event-B Modelling Language]]===


[[Event-B Mathematical Language]]
=== [[Event-B Mathematical Language]] ===
 
=== 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: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.