author : Didier Bert

Books

• ZB 2002. 2002, with Jonathan P. Bowen, Martin C. Henson, Ken Robinson
• ZB 2003. 2003, with Jonathan P. Bowen, Steve King, Marina Walden

Short works

• GeneSyst: a tool to reason about behavioral aspects of B Event specifications: aplication to security properties. 2005. (In ZB 2005 )

Books : reviews

Didier Bert, Jonathan P. Bowen, Martin C. Henson, Ken Robinson, eds.
ZB 2002: Formal Specification and Development in Z and B: Second International Conference of B and Z Users, Grenoble.
Springer. 2002

(read but not reviewed)

Contents

• Eric C. R. Hehner, Ioannis T. Kassios. Theories, Implementations, and Transformations. 2002

• Dominique Cansell, Ganesh Gopalakrishnan, Mike Jones, Dominique Mery, Airy Weinzoepflen. Incremental Proof of the Producer/Consumer Property for the PCI Protocol. 2002

• Michael Poppleton, Richard Banach. Controlling Control Systems: An Application of Evolving Retrenchment. 2002

• Neil J. Robinson. Checking Z Data Refinements Using an Animation Tool. 2002

• Graeme Smith, Florian Kammuller, Thomas Santen. Encoding Object-Z in Isabelle/HOL. 2002

• Ian Toyn, Susan Stepney. Characters + Mark-up = Z Lexis. 2002

full paper

• Marielle Doche, Andrew M. Gravell. Extraction of Abstraction Invariants for Data Refinement. 2002

• Leonid Mikhailov, Michael J. Butler. An Approach to Combining B and Alloy. 2002

• Ralph-Johan Back. Software Construction by Stepwise Feature Introduction. 2002

• Jim Woodcock, Ana L. C. Cavalcanti. The Semantics of Circus. 2002

• Ralph Miarka, John Derrick, Eerke A. Boiten. Handling Inconsistencies in Z Using Quasi-Classical Logic. 2002

• Eerke A. Boiten. Loose Specification and Refinement in Z. 2002

• Jean-Raymond Abrial, Louis Mussat. On Using Conditional Definitions in Formal Theories. 2002

• Steve Dunne. A Theory of Generalised Substitutions. 2002

• Sergiy A. Vilkomir, Jonathan P. Bowen. Reinforced Condition/Decision Coverage (RC/DC): A New Criterion for Software Testing. 2002

• Bruno Legeard, Fabien Peureux, Mark Utting. A Comparison of the BTT and TTF Test-Generation Methods. 2002

• David Basin, Frank Rittinger, Luca Vigano. A Formal Analysis of the CORBA Security Service. 2002

• Jean-Paul Bodeveix, Mamoun Filali. Type Synthesis in B and the Translation of B to PVS. 2002

• Jean-Raymond Abrial, Dominique Cansell, Guy Laffitte. "Higher-Order" Mathematics in B. 2002

• Pierre Chartier. ABS Project: Merging the Best Practices in Software Design from Railway and Aircraft Industries. 2002

• James Blow, Andy Galloway. Generalised Substitution Language and Differentials. 2002

• Steve Schneider, Helen Treharne. Communicating B Machines. 2002

• Francoise Bellegarde, Jacques Julliand, Olga Kouchnarenko. Synchronized Parallel Composition of Event Systems in B. 2002

• Antonis Papatsaras, Bill Stoddart. Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study. 2002

• Francoise Bellegarde, Samir Chouali, Jacques Julliand. Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions. 2002

• Soon-Kyeong Kim, David Carrington. A Formal Model of the UML Metamodel: The UML State Machine and Its Integrity Constraints. 2002

• Regine Laleau, Fiona Polack. Coming and Going from UML to B: A Proposal to Support Traceability in Rigorous IS Development. 2002

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