author : Didier Bert

Contents

• Eric C. R. Hehner, Ioannis T. Kassios.

Theories, Implementations, and Transformations

• Dominique Cansell, Ganesh Gopalakrishnan, Mike Jones, Dominique Mery, Airy Weinzoepflen.

Incremental Proof of the Producer/Consumer Property for the PCI Protocol

• Michael Poppleton, Richard Banach.

Controlling Control Systems: An Application of Evolving Retrenchment

• Neil J. Robinson.

Checking Z Data Refinements Using an Animation Tool

• Graeme Smith, Florian Kammuller, Thomas Santen.

Encoding Object-Z in Isabelle/HOL

• Ian Toyn, Susan Stepney.

Characters + Mark-up = Z Lexis

full paper

• Marielle Doche, Andrew M. Gravell.

Extraction of Abstraction Invariants for Data Refinement

• Leonid Mikhailov, Michael J. Butler.

An Approach to Combining B and Alloy

• Ralph-Johan Back.

Software Construction by Stepwise Feature Introduction

• Jim Woodcock, Ana L. C. Cavalcanti.

The Semantics of Circus

• Ralph Miarka, John Derrick, Eerke A. Boiten.

Handling Inconsistencies in Z Using Quasi-Classical Logic

• Eerke A. Boiten.

Loose Specification and Refinement in Z

• Jean-Raymond Abrial, Louis Mussat.

On Using Conditional Definitions in Formal Theories

• Steve Dunne.

A Theory of Generalised Substitutions

• Sergiy A. Vilkomir, Jonathan P. Bowen.

Reinforced Condition/Decision Coverage (RC/DC): A New Criterion for Software Testing

• Bruno Legeard, Fabien Peureux, Mark Utting.

A Comparison of the BTT and TTF Test-Generation Methods

• David Basin, Frank Rittinger, Luca Vigano.

A Formal Analysis of the CORBA Security Service

• Jean-Paul Bodeveix, Mamoun Filali.

Type Synthesis in B and the Translation of B to PVS

• Jean-Raymond Abrial, Dominique Cansell, Guy Laffitte.

"Higher-Order" Mathematics in B

• Pierre Chartier.

ABS Project: Merging the Best Practices in Software Design from Railway and Aircraft Industries

• James Blow, Andy Galloway.

Generalised Substitution Language and Differentials

• Steve Schneider, Helen Treharne.

Communicating B Machines

• Francoise Bellegarde, Jacques Julliand, Olga Kouchnarenko.

Synchronized Parallel Composition of Event Systems in B

• Antonis Papatsaras, Bill Stoddart.

Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study

• Francoise Bellegarde, Samir Chouali, Jacques Julliand.

Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions

• Soon-Kyeong Kim, David Carrington.

A Formal Model of the UML Metamodel: The UML State Machine and Its Integrity Constraints

• Regine Laleau, Fiona Polack.

Coming and Going from UML to B: A Proposal to Support Traceability in Rigorous IS Development

Contents

• Daniel Jackson.

Alloy: A Logical Modelling Language

(abstract, invited talk)

• Susan Stepney, Fiona Polack, Ian Toyn.

An Outline pattern language for Z: five illustrations and two tables

full paper

• Susan Stepney, Fiona Polack, Ian Toyn.

Patterns to guide practical refactoring: example targetting promotion in Z

full paper

• Sandrine Blazy, Frederic Gervais, Regine Laleau.

Reuse of specification patterns with the B method

• Helen Treharne, Steve Schneider, Marchia Bramble.

Composing specifications using communication

• Frederic Peschanski, David Julien.

When concurrent control meets functional requirements, or Z + Petri-nets

• Guilhem Pouzancre.

How to design a modern car with a formal B method?

• Stefan Hallerstede.

Parallel hardware design in B

• Moshe Deutsch, Martin C. Henson, Steve Reeves.

Operation refinement and monotonicity in the schema calculus

• John Derrick, Heike Wehrheim.

Using coupled simulations in non-atomic refinement

• Moshe Deutsch, Martin C. Henson.

An Analysis of forward simulation data refinement

• Jean-Raymond Abrial.

B#: Toward a Synthesis between Z and B

(invited talk)

• Steve Dunne.

Introducing backward refinement into B

• Bill Stoddart, Frank Zeyda.

Expression transformers in B-GSL

• Annabelle McIver, Carroll Morgan, Thai Son Hoang.

Probabilistic termination in B

• Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan.

Probabilistic invariants for probabilistic machines

• Graeme Smith, Kirsten Winter.

Proving temporal properties of Z specifications using abstraction

• Kirsten Winter, Graeme Smith.

Compositional verification for Object-Z

• John Derrick.

Timed CSP and Object-Z

• Mark Utting, Shaochun Wang.

Object orientation without extending Z

• Nuno Amalio, Fiona Polack.

Comparison of formalisation approaches of UML class constructs in Z and object-Z

(invited talk)

• Bertrand Meyer.

Towards practical proofs of class correctness

• Robert M. Hierons, Mark Harman, Harbhajan Singh.

Automatically generating information from a Z specification to support the classification tree method

• Christophe Darlot, Jacques Julliand, Olga Kouchnarenko.

Refinement preserves PLTL properties

• Marc Frappier, Regine Laleau.

Proving ordering properties for information systems

• Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, Nicholas Daley, David Currie.

ZML: XML support for standard Z

• Jean-Raymond Abrial, Dominique Cansell, Dominique Mery.

Formal derivation of spanning tree algorithms

• Carla Ferreira, Michael J. Butler.

Using B refinement to analyse compensating business processes

• Christine Poerschke, David E. Lightfoot, John L. Nealon.

A Formal specification in B of a medical decision support system

• Lilian Burdy, Antoine Requet.

Extending B with control flow breaks

• Nazareno Aguirre, Juan C. Bicarregui, Theo Dimitrakos, Thomas S. E. Maibaum.

Towards dynamic population management of abstract machines in the B method