Difference between revisions of "Event-B Language"

From Event-B
Jump to navigationJump to search
imported>WikiSysop
imported>WikiSysop
Line 22: 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 2 of ''Modeling in Event-B''] by Yoshio Tsukada.
  
 
== Event-B Language Documentation ==
 
== Event-B Language Documentation ==

Revision as of 11:20, 27 May 2011

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 2 of Modeling in Event-B by Yoshio Tsukada.

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

Well-definedness in Event-B

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.