Event-B Language: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Son
No edit summary
imported>Laurent
 
(14 intermediate revisions by 5 users not shown)
Line 1: Line 1:
== Book: Modelling in Event-B: System and Software Engineering by Jean-Raymond Abrial ==
== Book: Modeling in Event-B: System and Software Engineering by Jean-Raymond Abrial ==
=== Sample Chapters of the books ===
More information about the book is at Cambridge University Press [http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521895569 website].
This is available at event-b.org [http://www.event-b.org/abook.html]
 
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 ===
=== 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 1: [http://deploy-eprints.ecs.soton.ac.uk/111/ Introduction]
Line 17: Line 22:
* Chapter 16: [http://deploy-eprints.ecs.soton.ac.uk/123/ Location Access Controller]
* 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]
* 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]] ===


[http://wiki.event-b.org/images/EventB-Summary.pdf Concise Summary of the Event B mathematical toolkit] by Ken Robinson
=== 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==
==Modelling Tips==


[[Structured_Types]]
[[Structured_Types]]
[[Proof Hints]]


[[Category:User documentation]]
[[Category:User documentation]]

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.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_Language&oldid=4158’