## ZB 2002: Formal Specification and Development in Z and B: 2nd International Conference of B and Z Users Grenoble, France, January 23-25, 2002, ProceedingsDidier Bert, Jonathan P. Bowen, Martin C. Henson, Ken Robinson This book constitutes the refereed proceedings of the Second International Conference of B and Z Users, ZB 2002, held in Grenoble, France in January 2002. The 24 papers presented together with three invited contributions were carefully reviewed and selected for inclusion in the book. The book documents the recent advances for the Z formal specification notion and for the B method; the full scope is covered, ranging from foundational and theoretical issues to advanced applications, tools, and case studies. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Theories Implementations and Transformations | 1 |

Incremental Proof of the ProducerConsumer Property for the PCI Protocol | 22 |

An Application of Evolving Retrenchment | 42 |

Copyright | |

24 other sections not shown

### Other editions - View all

### Common terms and phrases

abstract allows Alloy applied approach axioms boolean C. A. R. Hoare calculus channel clause components Computer Science concrete constraints construct CORBA corresponding current-directory data refinement defined definition denotes diagram domain editors encoding END END environment event system example expression finite Formal Methods formal specification function generalised substitution implementation inconsistency initialisation input instantiation introduced invariant Isabelle/HOL J. C. P. Woodcock labeled transition system language Lemma LINKS LNCS logic machine mark-up MC/DC metamodel model checking notation Notes in Computer Object-Z Object-Z class operation output paraconsistent logics parallel composition parameters PLTL possible postcondition precondition predicate proof obligations properties queue refinement calculus relation requirements retrenchment rules schema semantics sequence SimpleText Springer-Verlag step structure subset Synch synchronization syntax theorem proving theory tion tool transaction transition system translation variables verification