Books

Short works

Books : reviews

Jonathan P. Bowen, Steve Dunne, Andy Galloway, Steve King, eds.
ZB 2000: Formal Specification and Development in Z and B: First International Conference of B and Z Users, York.
Springer. 2000

(read but not reviewed)

Contents

Soon-Kyeong Kim, David Carrington. A Formal Mapping between UML models and Object-Z Specifications. 2000
Regine Laleau, Amel Mammar. A Generic Process to Refine a B Specification into a Relational Database Implementation. 2000
Graeme Smith. Recursive Schema Definitions in Object­Z. 2000
Ian Toyn, Samuel H. Valentine, David A. Duffy. On Mutually Recursive Free Types in Z. 2000
David A. Duffy, Ian Toyn. Reasoning Inductively about Z Specifications via Unification. 2000
Ken Robinson. Reconciling Axomatic and Model­based Specifications Using the B Method. 2000
Theo Dimitrakos, Juan C. Bicarregui, Brian Matthews, Thomas S. E. Maibaum. Compositional structuring in the B Method: A Logical Viewpoint of the Static Context. 2000
Pierre Bontron, Marie-Laure Potet. Automatic Construction of Validated B components from Structured Developments. 2000
Dominique Cansell, Dominique Mery. Playing with abstraction and refinement for managing features interactions. 2000
Mark d'Inverno, Koen Hindriks, Michael Luck. A Formal Architecture for the 3APL Agent Programming Language. 2000
Helen Treharne, Steve Schneider. How to drive a B Machine. 2000
Nestor Lopez, Marianne Simonot, Veronique Viguie Donzeau-Gouge. Deriving Software Specifications from Event Based Models. 2000
Francoise Bellegarde, Christophe Darlot, Jacques Julliand, Olga Kouchnarenko. Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants. 2000
Samuel H. Valentine, Ian Toyn, Susan Stepney, Steve King. Type­constrained Generics for Z. 2000
full paper
Ian Toyn, Samuel H. Valentine, Susan Stepney, Steve King. Typechecking Z. 2000
full paper
Ralph Miarka, Eerke A. Boiten, John Derrick. Guards, Preconditions and Refinement in Z. 2000
Richard Banach, Michael Poppleton. Retrenchment, Refinement and Simulation. 2000
Michael J. Butler, Mairead Meagher. Performing Algorithmic Refinement before Data Refinement in B. 2000
Martin C. Henson, Steve Reeves. Program Development and Specification Refinement in the Schema Calculus. 2000
Jean-Louis Lanet. Are Smart Cards the Ideal Domain for Applying Formal Methods?. 2000
Susan Stepney, David Cooper. Formal Methods for Industrial Products. 2000
full paper
Bill Stoddart. An Execution Architecture for GSL. 2000
Wolfgang Grieskamp. A Computation Model for Z Based on Concurrent Constraint Resolution. 2000
Rob D. Arthan. Analysis of Compiled Code: A Prototype Formal Model. 2000
David Cooper, Susan Stepney. Segregation with Communication. 2000
full paper
David A. Duffy, Juergen Giesl. Closure Induction in a Z-like Language. 2000
Chris Matthews, Paul A. Swatman. Fuzzy Concepts and Formal Methods: A Fuzzy Logic Toolkit for Z. 2000

Didier Bert, Jonathan P. Bowen, Steve King, Marina Walden, eds.
ZB 2003: Formal Specification and Development in Z and B: Third International Conference of B and Z Users, Turku, Finland.
Springer. 2003

(read but not reviewed)

Contents

Daniel Jackson. Alloy: A Logical Modelling Language. 2003
(abstract, invited talk)
Susan Stepney, Fiona Polack, Ian Toyn. An Outline pattern language for Z: five illustrations and two tables. 2003
full paper
Susan Stepney, Fiona Polack, Ian Toyn. Patterns to guide practical refactoring: example targetting promotion in Z. 2003
full paper
Sandrine Blazy, Frederic Gervais, Regine Laleau. Reuse of specification patterns with the B method. 2003
Helen Treharne, Steve Schneider, Marchia Bramble. Composing specifications using communication. 2003
Frederic Peschanski, David Julien. When concurrent control meets functional requirements, or Z + Petri-nets. 2003
Guilhem Pouzancre. How to design a modern car with a formal B method?. 2003
Stefan Hallerstede. Parallel hardware design in B. 2003
Moshe Deutsch, Martin C. Henson, Steve Reeves. Operation refinement and monotonicity in the schema calculus. 2003
John Derrick, Heike Wehrheim. Using coupled simulations in non-atomic refinement. 2003
Moshe Deutsch, Martin C. Henson. An Analysis of forward simulation data refinement. 2003
Jean-Raymond Abrial. B#: Toward a Synthesis between Z and B. 2003
(invited talk)
Steve Dunne. Introducing backward refinement into B. 2003
Bill Stoddart, Frank Zeyda. Expression transformers in B-GSL. 2003
Annabelle McIver, Carroll Morgan, Thai Son Hoang. Probabilistic termination in B. 2003
Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan. Probabilistic invariants for probabilistic machines. 2003
Graeme Smith, Kirsten Winter. Proving temporal properties of Z specifications using abstraction. 2003
Kirsten Winter, Graeme Smith. Compositional verification for Object-Z. 2003
John Derrick. Timed CSP and Object-Z. 2003
Mark Utting, Shaochun Wang. Object orientation without extending Z. 2003
Nuno Amalio, Fiona Polack. Comparison of formalisation approaches of UML class constructs in Z and object-Z. 2003
(invited talk)
Bertrand Meyer. Towards practical proofs of class correctness. 2003
Robert M. Hierons, Mark Harman, Harbhajan Singh. Automatically generating information from a Z specification to support the classification tree method. 2003
Christophe Darlot, Jacques Julliand, Olga Kouchnarenko. Refinement preserves PLTL properties. 2003
Marc Frappier, Regine Laleau. Proving ordering properties for information systems. 2003
Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, Nicholas Daley, David Currie. ZML: XML support for standard Z. 2003
Jean-Raymond Abrial, Dominique Cansell, Dominique Mery. Formal derivation of spanning tree algorithms. 2003
Carla Ferreira, Michael J. Butler. Using B refinement to analyse compensating business processes. 2003
Christine Poerschke, David E. Lightfoot, John L. Nealon. A Formal specification in B of a medical decision support system. 2003
Lilian Burdy, Antoine Requet. Extending B with control flow breaks. 2003
Nazareno Aguirre, Juan C. Bicarregui, Theo Dimitrakos, Thomas S. E. Maibaum. Towards dynamic population management of abstract machines in the B method. 2003

Helen Treharne, Steve King, Martin C. Henson, Steve Schneider, eds.
ZB 2005: Formal Specification and Development in Z and B: Fourth International Conference of B and Z Users, Guildford, UK.
Springer. 2005

(read but not reviewed)

Contents

Cliff B. Jones. Specification before Satisfaction: the case for research into obtaining the right specification. 2005
(invited talk, extended abstract)
Michael Leuschel, Edd Turner. Visualising larger state spaces in ProB. 2005
John Derrick, Heike Wehrheim. Non-atomic refinement in Z and CSP. 2005
Steve Dunne, Stacey Conroy. Process refinement in B. 2005
Petra Malik, Mark Utting. CZT: a framework for Z tools. 2005
Graeme Smith, Luke Wildman. Model checking Z specifications using SAL. 2005
Ian Toyn, Andy Galloway. Proving properties of Stateflow models using ISO Standard Z and CADiZ. 2005
J. Christian Attiogbe. A stepwise development of the Peterson's mutual exclusion algorithm using B Abstract Systems. 2005
Pontus Bostrom, Marina Walden. An extension of Event B for developing Grid systems. 2005
Carroll Morgan, Thai Son Hoang, Jean-Raymond Abrial. The challenge of probabilistic Event B. 2005
(invited talk, extended abstract)
Jemima Rossmorris, Susan Stepney. Requirements as conjectures: intuitive DVD menu navigation. 2005
Frank Zeyda, Bill Stoddart, Steve Dunne. A Prospective-Value semantics for the GSL. 2005
Richard Banach, Simon Fraser. Retrenchment and the B-toolkit. 2005
Jean-Raymond Abrial, Dominique Cansell, Dominique Mery. Refinement and reachability in Event B. 2005
Soon-Kyeong Kim, David Carrington. A rigorous foundation for pattern-based design models. 2005
Nuno Amalio, Fiona Polack, Susan Stepney. An object-oriented structuring for Z based on Views. 2005
Yann Zimmermann, Diana Toma. Component reuse in B using ACL2. 2005
Didier Bert, Marie-Laure Potet, Nicolas Stouls. GeneSyst: a tool to reason about behavioral aspects of B Event specifications: aplication to security properties. 2005
Benjamin W. Long. Formal verification of a type flaw attack on a security protocol using Object-Z. 2005
Frederic Badeau, Arnaud Amelot. Using B as a high level programming language in an industrial project: Roissy VAL. 2005
(invited talk)
Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan. Development via refinement in Probabilistic B -- foundation and case study. 2005
Eerke A. Boiten, John Derrick. Formal program development with approximations. 2005
Lindsay Groves. Practical data refinement for the Z schema calculus. 2005
Ingo Bruckner, Heike Wehrheim. Slicing Object-Z specifications for verification. 2005
Fabrice Bouquet, Frederic Dadeau, Julien Groslambert. Checking JML specifications with B Machines. 2005
Judy Bowen, Steve Reeves. Including design guidelines in the formal specification of interfaces in Z. 2005
Abdolbaghi Rezazadeh, Michael J. Butler. Some guidelines for formal development of web-based applications in the B-Method. 2005