Event-B Language: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>WikiSysop |
imported>Laurent |
||
| (30 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== | ==Modelling Tips== | ||
[[Structured_Types]] | [[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
- Chapter 1: Introduction
- Chapter 2: Controlling Cars on a Bridge
- Chapter 3: A Mechanical Press Controller
- Chapter 4: File Transfer Protocol
- Chapter 6: The Bounded Re-transmission Protocol
- Chapter 7: Concurrent Program Development
- Chapter 8: Electronic Circuits Development
- Chapter 10: Leader Election on a Ring-shaped Network
- Chapter 11: Synchronizing Processes on a Tree Network
- Chapter 12: Routing Algorithm for Mobile Agent
- Chapter 13: The Leader Election Protocol (IEEE1394)
- Chapter 15: Sequential Program Development
- Chapter 16: Location Access Controller
- Chapter 17: Train System
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
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.
