Prologue: faultless systems – yes we can!; Acknowledgements; 1. Introduction; 2. Controlling cars on a bridge; 3. A mechanical press controller; 4. A simple file transfer protocol; 5. The Event-B modeling notation and proof obligations rules; 6. Bounded re-transmission protocol; 7. Development of a concurrent program; 8. Development of electronic circuits; 9. Mathematical language; 10. Leader election on a ring-shaped network; 11. Synchronizing a tree-shaped network; 12. Routing algorithm for a mobile agent; 13. Leader election on a connected graph network; 14. Mathematical models for proof obligations; 15. Development of sequential programs; 16. A location access controller; 17. Train system; 18. Problems; Index.
A practical introduction to this model-based formal method, containing a broad range of illustrative examples.
Jean-Raymond Abrial is a researcher in the Department of Computer Science at ETH Zürich.
'This present book is the definitive treatment of the new B
dialect, written by its creator. Unlike its classical B predecessor
which is intended as a reference for the classical B methodology,
the present volume is squarely aimed at teaching, though the
considerably lighter theory of Event-B permits some of the chapters
to act as a reference too.' logcom.oxfordjournals.org
'… a rich and accessible book, demonstrating both the strengths and
weaknesses of the use of Event-B, and containing varied and
valuable case studies as its core. It is written in a pleasant
colloquial style, with changes in the vocal tempo and tone leaping
off the pages. … should be seriously considered for introductory
courses on formal modelling with associated proof.' Journal of
Functional Programming
 |
Ask a Question About this Product More... |
|
