home > book reviews > Steve King
Google > Steve King


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