imported>WikiSysop |
|
| Line 1: |
Line 1: |
| − | == Book: Modeling in Event-B: System and Software Engineering by Jean-Raymond Abrial ==
| + | Slides from Steve Wright's presentation "Experiences with a Quite Big Event-b Model", given at the Rodin workshop, Southampton, July 16th 2009. |
| − | 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 Modelling 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.] ===
| |
| − | | |
| − | === [http://wiki.event-b.org/images/EventB-Summary.pdf Concise Summary of the Event B mathematical toolkit] by Ken Robinson ===
| |
| − | | |
| − | ==Modelling Tips==
| |
| − | | |
| − | [[Structured_Types]]
| |
| − | | |
| − | [[Proof Hints]]
| |
| − | | |
| − | [[Category:User documentation]]
| |
| − | [[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].
| |
