author : Jonathan P. Bowen

Contents

• Dan Craigen, Susan Gerhart, Ted Ralston.

An International Survey of Industrial Applications of Formal Methods

(invited talk)

• Samuel H. Valentine.

Putting Numbers into the Mathematical Toolkit

• Ian J. Hayes, Luke Wildman.

Towards Libraries for Z

• John E. Nicholls.

Plain Guide to the Z Base Standard

• Kevin C. Lano, Howard Haughton.

Reuse and Adaptation of Z Specifications

• Andrew Bradley.

Requirements for Defence Standard 00-55

(invited talk: abstract)

• Jonathan Jacky.

Formal Specification and Development of Control System Input/Output

• John C. Knight, Darrell M. Kienzle.

Preliminary Experience Using Z to Specify a Safety-Critical System

• Andrew C. Coombes, John A. McDermid.

Using Diagrams to Give a Formal Specification of Timing Constraints in Z

• Alastair R. Ruddle.

Formal Methods in the Specification of Real-Time, Safety-Critical Control Systems

• I. Maung, J. R. Howse.

Introducing Hyper-Z -- A New Approach to Object-Orientation in Z

• G. Hossein Bagherzadeh Rafsanjani, S. J. Colwill.

From Object-Z to C++: A Structural Mapping

• Elspeth Cusack, Clazien Wezeman.

Deriving Tests for Objects Specified in Z

• Elspeth Cusack.

Using Z in Communications Engineering

(invited talk)

• Paul A. Swatman.

Using Formal Specification in the Acquisition of Information Systems: Educating Information Systems Professionals

• Christine Draper.

Practical Experiences of Z and SSADM

• Rosalind Barden, Susan Stepney.

Support for using Z

full paper

• Glyn Normington.

Cleanroom and Z

(invited talk)

• Matthew Love.

Animating Z Specifications in SQL*Forms3.0

Contents

• Robert Worden.

Fermenting and Distilling

• Jim Woodcock, Paul H. B. Gardiner, J.R. Hulance.

The Formal Specification in Z of Defence Standard 00-56

• Peter Mataga, Pamela Zave.

Formal Specification of Telephone Features

• David Carrington, Phil Stocks.

A Tale of Two Paradigms: Formal Methods and Software Testing

• David Garlan.

Integrating Formal Methods into a Professional Master of Software Engineering Program

• Graeme Smith.

An Object-Oriented Development Framework for Z

• Clazien Wezeman, Tony J. Judge.

Z for Managed Objects

• J. Anthony Hall.

Specifying and Interpreting Class Hierarchies in Z

• Jonathan P. Bowen, Mike J. C. Gordon.

Z and HOL

• Peter Baumann.

Z and Natural Semantics

• Peter T. Breuer, Jonathan P. Bowen.

Towards Correct Executable Semantics for Z

• Jon G. Hall, John A. McDermid.

Towards a Z Method: Axiomatic Specifications in Z

• Fiona Polack, Keith C. Mander.

Software Quality Assurance Using the SAZ Method

• Antoni Diller, Rosemary Docherty.

Z and Abstract Machine Notation: A Comparison

• Leslie Lamport.

TLZ (abstract)

• Andy S. Evans.

Visualising Concurrent Z Specifications

• Marcin Engel.

Specifying Real-Time Systems with Z and the Duration Calculus

• Daniel K. C. Chan, Philip W. Trinder.

An Object-Oriented Data Model Supporting Multi-Methods, Multiple Inheritance, and Static Type Checking: A Specification in Z

• Jonathan Hammond.

Producing Z Specifications from Object-Oriented Analysis

• W. Hasselbring.

Animation of Object-Z Specifications with a Set-Oriented Prototyping Language

Contents

• Michael G. Hinchey, Jonathan P. Bowen.

Applications of Formal Methods FAQ

• David L. Parnas.

Using Mathematical Models in the Inspection of Critical Software

• Glenn Bruns, Stuart Anderson.

Gaining Assurance with Formal Methods

• David Garlan, Norman Delisle.

Formal Specification of an Architecture for a Family of Instrumentation Systems

• Paul Mukherjee, Brian A. Wichmann.

Formal Specification of the STV Algorithm

• Jonathan P. Hoare.

Application of the B-Method to CICS

• Mandayam K. Srivas, Steve P. Miller.

Formal Verification of the AAMP5 Microprocessor

• William D. Young.

Modeling and Verification of a Simple Real-Time Gate Controller

• Eugene H. Durr, Nico Plat, Michiel de Boer.

CombiCom: Tracking and Tracing Rail Traffic using VDM++

• Babak Dehbonei, Fernando Mejia.

Formal Development of Safety-Critical Software Systems in Railway Signaling

• Ute Hamer, Jan Peleska.

Z Applied to the A330/340 CIDS Cabin Communication System

• David Guaspari, Mike Seager, Matt Stillerman.

Specifying the Kernel of a Secure Distributed Operating System

• Andrew C. Coombes, Leonor Barroca, John S. Fitzgerald, John A. McDermid, Lynne Spencer, Amer Saed.

Formal Specification of an Aerospace System: The Attitude Monitor

• John S. Fitzgerald, Peter Gorm Larsen, Tom Brookes, Michael Green.

Developing a Security-Critical System using Formal and Conventional Methods

• Vivien Hamilton.

The Use of Z within a Safety-Critical Software System

• Peter Mataga, Pamela Zave.

Multiparadigm Specification of an AT&T Switching System

• Dan Craigen, Susan Gerhart, Ted Ralston.

Formal Methods Technology Transfer: Impediments and Innovation

Contents

• Pascal Bernard, Guy Laffitte.

The French Population Census for 1990

• David L. Parnas.

Language-free mathematical methods for software design (extended abstract)

• Paolo Ciaccia, Paolo Ciancarini, W. Penzo.

A Formal approach to software design: the Clepsydra methodology

• David Edmond.

Refining database systems

• Michael Luck, Mark d'Inverno.

Structuring a Z specification to provide a formal framework for autonomous agent systems

• Patricia Duarte de Lima Machado, Silvio Lemos Meira.

On the use of formal specifications in the design and simulation of artificial neural networks

• Mark d'Inverno, Mark Priestley.

Structuring specification in Z to build a unifying framework for hypertext systems

• John M. Rushby.

Mechanizing Formal Methods: opportunities and challenges

• A. P. Hughes, A. A. Donnelly.

An Algebraic proof in VDM*

• Susan Stepney.

Testing as Abstraction

full paper

• Hans-Martin Horcher.

Improving software tests using Z specifications

• Erich Mikk.

Compilation of Z specifications into C for automatic test result evaluation

• Samuel H. Valentine.

Equal Rights for schemas in Z

• Anthony MacDonald, David Carrington.

Structuring Z Specifications: some choices

• Daniel M. German, D. D. Cowan.

Experiments with the Z Interchange Format and SGML

• Barbara Liskov, Jeannette M. Wing.

Specifications and Their Use in Defining Subtypes

• Ben Strulo.

How Firing Conditions Help Inheritance

• Graeme Smith.

Extending W for Object-Z

• Peter Bancroft, Ian J. Hayes.

A Formal Semantics for a Language with Type Extension

• Jonathan Jacky, Jonathan Unger.

From Z to Code: A Graphical User Interface for a Radiation Therapy Machine

• Ina Kraan, Peter Baumann.

Implementing Z in Isabelle

• Howard S. Goodman.

The Z-into-Haskell Tool-Kit: an illustrative case study

• Margaret M. West.

Types and Sets in Godel and Z

• Colman Reilly.

Exploring Specifications with Mathematica

• Tony Bryant, Andy S. Evans, Lesley Semmens, Rajko Milovanovic, Sinclair Stockman, Mark Norris, Clive Selley.

Using Z to Rigorously Review a Specification of a Network Management System

• Robert B. France, M. M. Larrondo-Petrie.

A Two-Dimensional View of Integrated Formal and Informal Specification Techniques

• John Derrick, Howard Bowman, Maarten Steen.

Viewpoints and Objects

• David L. Parnas.

Teaching Programming as Engineering

• Paolo Ciancarini, Paolo Ciaccia.

A Course on Formal Methods in Software Engineering: Matching Requirements with Design

• Jeannette M. Wing.

Hints for Writing Specifications (abstract)

• Neville Dean.

Mental Models of Z: I - Sets and Logic

• David Gries.

Equational Logic: A Great Pedagogical Tool for Teaching a Skill in Logic (abstract)

• Lubos Mikusiak, Vladimir Vojtek, Jozef Hasaralejko, Jana Hanzelova.

Z Browser - Tool for Visualization of Z Specifications

Contents

• Constance Heitmeyer.

Formal Methods: Panacea or Academic Poppycock?

• Bill Stoddart.

The Event Calculus

• M. A. Hewitt, Colin M. O'Halloran, Chris T. Sennett.

Experiences with PiZA, an animator for Z

• Steffen Helke, Thomas Neustupny, Thomas Santen.

Automating Test Case Generation from Z Specifications with Isabelle

• Mark Saaltink.

The Z/EVES System

• J. Anthony Hall.

Taking Z Seriously

(extended abstract)

• Klaus Achatz, Wolfram Schulte.

A Formal OO Method inspired by Fusion and Object-Z

• Jon G. Hall, Andrew Martin.

W Reconstructed

• Ina Kraan.

Using the Rippling Heuristic in Set Membership Proofs

• Egon Borger, S. Mazzanti.

A Practical Method for Rigorously Controllable Hardware Design

• Kevin C. Lano, Stephen J. Goldsack, Juan C. Bicarregui, Stuart J. H. Kent.

Integrating VDM++ and Real-Time System Design

• Michael J. Butler.

An Approach to the Design of Distributed Systems with B AMN

• Kevin C. Lano.

Specifying Reactive Systems in B AMN

• Andy S. Evans.

An Improved Recipe for Specifying Reactive Systems in Z

• Mark d'Inverno, Michael Hu.

A Z Specification of the Soft-Link Hypertext Model

• Jonathan Jacky, Jonathan Unger, Michael Patrick, David Reid, Ruedi Risler.

Experience with Z developing a Control Program for a Radiation Therapy Machine

• John C. Knight, Susan S. Brilliant.

Preliminary Evaluation of a Formal Approach to User Interface Specification

• Paolo Ciancarini, Cecilia Mascolo.

Analysing and Refining an Architectural Style

• John Derrick, Eerke A. Boiten, Howard Bowman, Maarten Steen.

Weak Refinement in Z

Contents

• Klaus Grimm.

Industrial Requirements for the Efficient Development of Reliable Embedded Systems

• Clemens Fischer.

How to Combine Z with a Process Algebra

• Bill Stoddart.

The Specification and Refinement of an Environmental Model

• Leesa Murray, David Carrington, Ian MacColl, Jason McDonald, Paul A. Strooper.

Formal Derivation of Finite State Machines for Class Testing

• Ib Holm Sorensen.

Using B to Specify, Verify and Design Hardware Circuits

• Jonathan P. Bowen, David Chippington.

Z on the Web Using Java

• Paolo Ciancarini, Cecilia Mascolo, Fabio Vitali.

Visualizing Z Notation in HTML Documents

• Thomas Santen.

On the Semantic Relation of Z and HOL

• C. Luth, E. W. Karlsen, Kolyang, S. Westmeier, B. Wolff.

HOL-Z in the UniForM-Workbench - A Case Study in Tool Integration for Z

• Jonathan Jacky.

Analyzing a Real-Time Program with Z

• Rob D. Arthan.

Recursive Definitions in Z

• Martin C. Henson, Steve Reeves.

A Logic for the Schema Calculus

• Ian Toyn.

Innovations in the Notation of Standard Z

• Richard F. Paige.

Comparing Extended Z with a Heterogeneous Notation for Reasoning about Time and Space

• Samuel H. Valentine.

Inconsistency and Undefinedness in Z - A Practical Guide

• Kevin C. Lano, P. Kan, Arturo Sanchez.

Compositional Specification of Controllers for Batch Process Operations

• John Derrick, Eerke A. Boiten.

Testing Refinements by Refining Tests

• Susan Stepney, David Cooper, Jim Woodcock.

More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement

full paper

• Brendan P. Mahony, Jin Song Dong.

Network Topology and a Case Study in TCOZ

• Viktor Friesen, Andre Nordwig, Matthias Weber.

Object-Oriented Specification of Hybrid Systems Using UMLh and ZimOO

• S. Dupuy, Y. Ledru, M. Chabre-Peccoud.

Translating the OMT Dynamic Model into Object-Z

Contents

• Jonathan P. Bowen, Michael G. Hinchey.

It's Greek to Me: Method in the Madness?

• Pascal Bernard, Guy Laffitte.

The French Population Census for 1990

• Ross J. Anderson.

The Formal Verification of a Payment System

• Kevin C. Lano, Stephen J. Goldsack, Arturo Sanchez.

Specification of a Chemical Process Controller in B

• Bishop C. Brock, Warren A. Hunt Jr.

Formal Analysis of the Motorola CAP DSP

• Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan.

Bridging the E-Business Gap Through Formal Verification

• Nancy G. Leveson, Mats P. E. Heimdahl, Jon D. Reese.

A CAD Environment for Safety-Critical Software

• Dines Bjorner, Chris George, Soren Prehn.

Scheduling and Rescheduling of Trains

• Jonathan Jacky.

Lessons from the Formal Development of a Radiation Therapy Machine Control Program

• J. Anthony Hall.

Using Formal Methods to Develop an ATC Information System

• Lesley Semmens, Tony Bryant.

Rigorous Review Technique

• Dan Craigen, Irwin Meisels, Mark Saaltink.

Analysing Z Specifications with Z/EVES

• Andrew P. Moore, J. Eric Klinker, David M. Mihelcic.

How to Construct Formal Arguments that Persuade Certifiers

• Mark Ardis, Peter Mataga.

Formal Methods Through Domain Engineering

• Arne Boralv, Gunnar Stalmarck.

Formal Verification in Railways

• Richard C. Linger, Carmen J. Trammell.

Cleanroom Software Engineering: Theory and Practice

Contents

• Soon-Kyeong Kim, David Carrington.

A Formal Mapping between UML models and Object-Z Specifications

• Regine Laleau, Amel Mammar.

A Generic Process to Refine a B Specification into a Relational Database Implementation

• Graeme Smith.

Recursive Schema Definitions in Object­Z

• Ian Toyn, Samuel H. Valentine, David A. Duffy.

On Mutually Recursive Free Types in Z

• David A. Duffy, Ian Toyn.

Reasoning Inductively about Z Specifications via Unification

• Ken Robinson.

Reconciling Axomatic and Model­based Specifications Using the B Method

• Theo Dimitrakos, Juan C. Bicarregui, Brian Matthews, Thomas S. E. Maibaum.

Compositional structuring in the B Method: A Logical Viewpoint of the Static Context

• Pierre Bontron, Marie-Laure Potet.

Automatic Construction of Validated B components from Structured Developments

• Dominique Cansell, Dominique Mery.

Playing with abstraction and refinement for managing features interactions

• Mark d'Inverno, Koen Hindriks, Michael Luck.

A Formal Architecture for the 3APL Agent Programming Language

• Helen Treharne, Steve Schneider.

How to drive a B Machine

• Nestor Lopez, Marianne Simonot, Veronique Viguie Donzeau-Gouge.

Deriving Software Specifications from Event Based Models

• Francoise Bellegarde, Christophe Darlot, Jacques Julliand, Olga Kouchnarenko.

Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants

• Samuel H. Valentine, Ian Toyn, Susan Stepney, Steve King.

Type­constrained Generics for Z

full paper

• Ian Toyn, Samuel H. Valentine, Susan Stepney, Steve King.

Typechecking Z

full paper

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

Guards, Preconditions and Refinement in Z

• Richard Banach, Michael Poppleton.

Retrenchment, Refinement and Simulation

• Michael J. Butler, Mairead Meagher.

Performing Algorithmic Refinement before Data Refinement in B

• Martin C. Henson, Steve Reeves.

Program Development and Specification Refinement in the Schema Calculus

• Jean-Louis Lanet.

Are Smart Cards the Ideal Domain for Applying Formal Methods?

• Susan Stepney, David Cooper.

Formal Methods for Industrial Products

full paper

• Bill Stoddart.

An Execution Architecture for GSL

• Wolfgang Grieskamp.

A Computation Model for Z Based on Concurrent Constraint Resolution

• Rob D. Arthan.

Analysis of Compiled Code: A Prototype Formal Model

• David Cooper, Susan Stepney.

Segregation with Communication

full paper

• David A. Duffy, Juergen Giesl.

Closure Induction in a Z-like Language

• Chris Matthews, Paul A. Swatman.

Fuzzy Concepts and Formal Methods: A Fuzzy Logic Toolkit for Z

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