Books

Short works

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