home > book reviews > Jim Woodcock
Google > Jim Woodcock


Books

Short works

Books : reviews

Jim Woodcock, Jim Davies.
Using Z: specification, refinement, and proof.
Prentice-Hall. 1996

+

(read but not reviewed)

This book contains enough material for three complete courses of study. It provides an introduction to the world of logic, sets and relations. It explains the use of the Z notation in the specification of realistic systems. It shows how Z specifications may be refined to produce executable code; this is demonstrated in a selection of case studies.

This title is both authoritative and comprehensive. It strikes the right balance between the formality of mathematics and the practical needs of industrial software development. It is faithful to the draft ISO standard for Z. It covers the essentials of specification, refinement, and proof, revealing techniques never previously published.

This book is based upon the experience of the authors in teaching Z to a wide variety of audiences. Many of their students have produced large, industrial specifications in Z; some have even produced their own textbooks.

Jeannette M. Wing, Jim Woodcock, Jim Davies, eds.
FM'99 volume 1: World Congress on Formal Methods, Toulouse, September 1999.
Springer. 1999

(read but not reviewed)

Contents

• C. A. R. Hoare. Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle. 1999
• Cliff B. Jones. Scientific Decisions which Characterize VDM. 1999
• John M. Rushby. Mechanized Formal Methods: Where Next?. 1999
• Joseph Sifakis. Integration, the Price of Success (extended abstract). 1999
• Michael Jackson. The Role of Formalism in Method (abstract). 1999
• Eric Conquet, Jean-Luc Marty. Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project.. 1999
• Henk Eertink, Wil Janssen, Paul Oude Luttighuis, Wouter B. Teeuw, Chris A. Vissers. A Business Process Design Language. 1999
• Jan Philipps, Bernhard Rumpe. Refinement of Pipe-and-Filter Architectures. 1999
• John Herbert, Bruno Dutertre, Robert A. Riemenschneider, Victoria Stavridou. A Formalization of Software Architecture. 1999
• Reino Kurki-Suonio. Component and Interface Refinement in Closed-System Specifications. 1999
• Dusko Pavlovic. Semantics of First Order Parametric Specifications. 1999
• Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan. A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. 1999
• Frank Reffel, Stefan Edelkamp. Error Detection with Directed Symbolic Model Checking. 1999
• Rajeev Alur, Joel M. Esposito, M. Kim, Vijay Kumar, Insup Lee. Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination. 1999
• Stavros Tripakis, Karine Altisen. On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems. 1999
• Jean-Michel Couvreur. On-the-Fly Verification of Linear Temporal Logic. 1999
• David Deharbe, Anamaria Martins Moreira. Symbolic Model Checking with Fewer Fixpoint Computations. 1999
• Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, Gigliola Vaglini. Formula Based Abstractions of Transition Systems for Real-Time Model Checking. 1999
• Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier. IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. 1999
• Farn Wang. Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes. 1999
• Denis Sabatier, Pierre Lartigue. The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications. 1999
• Patrick Behm, Paul Benoit, Alain Faivre, Jean-Marc Meynadier. Meteor: A Successful Application of B in a Large Project. 1999
• Brian Matthews, Elvira Locuratolo. Formal Development of Databases in ASSO and B. 1999
• Yann Rouzaud. Interpreting the B-Method in the Refinement Calculus. 1999
• Martin Buchi, Ralph-Johan Back. Compositional Symmetric Sharing in B. 1999
• Cesar Munoz,, John M. Rushby. Structural Embeddings: Mechanization with Method. 1999
• Steve Dunne. The Safe Machine: A New Specification Construct for B. 1999
• Michael J. Butler. csp2B: A Practical Approach to Combining CSP and B. 1999
• Salimeh Behnia, Helene Waeselynck. Test Criteria Definition for B Models. 1999
• Richard F. Paige, Eric C. R. Hehner. Bunches for Object-Oriented, Concurrent, and Real-Time Specification. 1999
• Enn Tyugu, Mihhail Matskin, Jaan Penjam. Applications of Structural Synthesis of Programs. 1999
• Michel Charpentier, K. Mani Chandy. Towards a Compositional Approach to the Design and Verification of Distributed Systems. 1999
• Andre Wong, Marsha Chechik. Formal Modeling in a Commercial Setting: A Case Study. 1999
• Igor Burdonov, Alexander Kossatchev, Alexandre Petrenko, Dmitri Galter. KVEST: Automated Generation of Test Suites from Formal Specifications. 1999
• Lydie du Bousquet. Feature Interaction Detection Using Testing and Model-Checking Experience Report. 1999
• Nisse Husberg, Tapio Manner. Emma: Developing an Industrial Reachability Analyser for SDL. 1999
• Jean-Francois Monin, Francis Klay. Correctness Proof of the Standardized Algorithm for ABR Conformance. 1999
• Thomas Arts, Mads Dam. Verifying a Distributed Database Lookup Manager Written in Erlang. 1999
• Fred Gilham, Robert A. Riemenschneider, Victoria Stavridou. Secure Interoperation of Secure Distributed Databases. 1999
• Volkmar Lotz, Volker Kessler, Georg Walter. A Formal Security Model for Microprocessor Hardware. 1999
• Steve Schneider. Abstraction and Testing. 1999
• Dan Zhou, Shiu-Kai Chin. Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol. 1999
• Patrick Lincoln, John C. Mitchell, Mark Mitchell, Andre Scedrov. Probabilistic Polynomial-Time Equivalence and Security Analysis. 1999
• Riccardo Focardi, Fabio Martinelli. A Uniform Approach for the Definition of Security Properties. 1999
• Paul F. Syverson, Stuart G. Stubblebine. Group Principals and the Formalization of Anonymity. 1999
• Richard F. Paige, Jonathan S. Ostroff. Developing BON as an Industrial-Strength Formal Method. 1999
• Luis Mandel, Maria Victoria Cengarle. On the Expressive Power of OCL. 1999
• Eric Meyer, Jeanine Souquieres. A Systematic Approach to Transform OMT Diagrams to a B Specification. 1999
• Shaoying Liu. Verifying Consistency and Validity of Formal Specifications by Testing. 1999
• Marine Tabourier, Ana R. Cavalli, Melania Ionescu. A GSM-MAP Protocol Experiment Using Passive Testing. 1999

Jeannette M. Wing, Jim Woodcock, Jim Davies, eds.
FM'99 volume 2: World Congress on Formal Methods, Toulouse, September 1999.
Springer. 1999

(read but not reviewed)

Contents

• Pascal Poizat, Christine Choppy, Jean-Claude Royer. From Informal Requirements to COOP: A Concurrent Automata Approach. 1999
• Frederic Lang, Pierre Lescanne, Luigi Liquori. A Framework for Defining Object-Calculi. 1999
• Sanjit Arunkumar Seshia, R. K. Shyamasundar, A. K. Bhattacharjee, S. D. Dhodapkar. A Translation of Statecharts to Esterel. 1999
• Xia Yong, Chris George. An Operational Semantics for Timed RAISE. 1999
• Heike Wehrheim. Data Abstraction for CSP-OZ. 1999
• Fiona Polack, Susan Stepney. Systems Development Using Z Generics. 1999
full paper
• Perry Alexander, Murali Rangarajan, Phillip Baraona. A Brief Summary of VSPEC. 1999
• Gary T. Leavens, Albert L. Baker. Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. 1999
• Markus Muller-Olm, Andreas Wolf. On Excusable and Inexcusable Failures. 1999
• Richard Verhoeven, Roland Carl Backhouse. Interfacing Program Construction and Verification. 1999
• S. Dellacherie, Samuel Devulder, Jean-Luc Lambert. Software Verification Based on Linear Programming. 1999
• Brendan P. Mahony, Jin Song Dong. Sensors and Actuators in TCOZ. 1999
• Bernd Krieg-Bruckner, Jan Peleska, Ernst-Rudiger Olderog, Alexander Baer. The UniForM Workbench, a Universal Development Environment for Formal Methods. 1999
• Bernhard Schatz, Franz Huber. Integrating Formal Description Techniques. 1999
• Stephan Merz. A More Complete TLA. 1999
• Frank S. de Boer, Ulrich Hannemann, Willem-Paul de Roever. Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach. 1999
• Andrew Martin. Relating Z and First-Order Logic. 1999
• Joao Pedro Sousa, David Garlan. Formal Modeling of the Enterprise JavaBeansTM Component Integration Framework. 1999
• Leonid Mikhajlov, Emil Sekerinski, Linas Laibinis. Developing Components in the Presence of Re-entrance. 1999
• H. B. M. Jonkers. Communication and Synchronisation Using Interaction Objects. 1999
• Loe M. G. Feijs. Modelling Microsoft COM Using pi-Calculus. 1999
• Irina M. Smarandache, Thierry Gautier, Paul Le Guernic. Validation of Mixed SIGNAL-ALPHA Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints. 1999
• Simin Nadjm-Tehrani, Ove Akerlund. Combining Theorem Proving and Continuous Models in Synchronous Design. 1999
• Juliano Iyoda, Augusto Sampaio, Leila Silva. ParTS: A Partitioning Transformation System. 1999
• He Jifeng. A Behavioral Model for Co-design. 1999
• Ana L. C. Cavalcanti, David A. Naumann. A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. 1999
• Ralph-Johan Back, Anna Mikhajlova, Joakim von Wright. Reasoning About Interactive Systems. 1999
• John Derrick, Eerke A. Boiten. Non-atomic Refinement in Z. 1999
• Eric C. R. Hehner, Andrew M. Gravell. Refinement Semantics and Loop Rules. 1999
• Michel R. V. Chaudron, Jan Tretmans, Klaas Wijbrans. Lessons from the Application of Formal Methods to the Design of a Storm Surge Barrier Control System. 1999
• Steve King, Jonathan Hammond, Rod Chapman, Andy Pryor. The Value of Verification: Positive Experience of Industrial Proof. 1999
• Anne Elisabeth Haxthausen, Jan Peleska. Formal Development and Verification of a Distributed Railway Control System. 1999
• Kaisa Sere, Elena Troubitsyna. Safety Analysis in Formal Specification. 1999
• Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita. Formal Specification and Validation of a Vital Communication Protocol. 1999
• Herve Marchand, Mazen Samaan. Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology. 1999
• Akira Mori, Kokichi Futatsugi. Verifying Behavioural Specifications in CafeOBJ Environment. 1999
• Razvan Diaconescu, Kokichi Futatsugi, Shusaku Iida. Component-Based Algebraic Specification and Verification in CafeOBJ. 1999
• Shin Nakajima. Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks. 1999
• Manuel Clavel, Fransisco Duran, Steven Eker, Jose Meseguer, Mark-Oliver Stehr. Maude as a Formal Meta-tool. 1999
• Joseph A. Goguen, Grigore Rosu. Hiding More of Hidden Algebra. 1999
• Robert Eschbach. A Termination Detection Algorithm: Specification and Verification. 1999
• Erich Gradel, Marc Spielmann. Logspace Reducibility via Abstract State Machines. 1999
• Martin Dunstan, Tom Kelsey, Ursula Martin, Steve Linton. Formal Methods for Extensions to CAS. 1999
• Rosa M. Jimenez, Fernando Orejas. An Algebraic Framework for Higher-Order Modules. 1999
• Famantanantsoa Randimbivololona, Jean Souyris, Patrick Baudin, Anne Pacalet, Jacques Raguideau, Dominique Schoen. Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. 1999
• P. Garbett, J. P. Parkes, M. Shackleton, Stuart Anderson. Secure Synthesis of Code: A Process Improvement Experiment. 1999
• Olivier Hainque, Laurent Pautet, Yann Le Biannic, Eric Nassor. Cronos: A Separate Compilation Toolset for Modular Esterel Applications. 1999

Jim Davies, A. W. Roscoe, Jim Woodcock, eds.
Millennial Perspectives in Computer Science: proceedings of the 1999 Oxford-Microsoft symposium in honour of Sir Tony Hoare.
Prentice-Hall. 2000

Contents

• Samson Abramsky. Concurrent interaction games. 2000
• Richard S. Bird, Jeremy Gibbons, Geraint Jones. Program optimisation, naturally. 2000
• Dines Bjorner. Domain modelling. 2000
• Richard P. Brent. The binary Euclidean algorithm. 2000
• Stephen Brookes. Communicating Parallel Processes. 2000
• Stephen Cameron. Computing with shapes. 2000
• K. Mani Chandy, Michel Charpentier. Predicate transformers for composition. 2000
• Ole-Johan Dahl. A note on monitor versions. 2000
• Edsger W. Dijkstra. A formula is worth a thousand pictures. 2000
• Mike J. C. Gordon. Linking higher order logic to binary decision diagrams. 2000
• David Gries, Fred B. Schneider. Substitution of equals for equals. 2000
• He Jifeng, Xu Qiwen. Advanced features of the duration calculus. 2000
• Eric C. R. Hehner. Formalism and the variable. 2000
• Michael Jackson. The real world. 2000
• Cliff B. Jones. Compositionality, interference and concurrency. 2000
• Donald E. Knuth. Dancing links. 2000
• David May. The transputer revisited. 2000
• Bertrand Meyer. Principles of language design and evolution. 2000
• Robin Milner. Computing and communication-what's the difference?. 2000
• Jayadev Misra. Generating-functions of interconnection networks. 2000
• Carroll Morgan, Annabelle McIver, J. W. Sanders. Probably Hoare? Hoare probably!. 2000
• Roger M. Needham. Distributed computing: opportunity, challenge, or misfortune?. 2000
• C.-H. L. Ong, A. S. Murawski. A linear-time algorithm for verifying MLL proof nets. 2000
• John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. 2000
• A. W. Roscoe, G. M. Reed, R. Forster. The successes and failures of behavioural models. 2000
• J. Michael Spivey, Silvija Seres. The algebra of searching. 2000
• Bernard Sufrin, Oege de Moor. Modeless structure editing. 2000
• Antti Valmari. A chaos-free failures-divergences semantics. 2000
• Niklaus Wirth. Records, modules, objects, classes, components. 2000
• Jim Woodcock, Jim Davies, Christie Bolton. Abstract data types and processes. 2000
• Zhou Chaochen, Dimitar P. Guelev, Zhan Naijun. A higher-order duration calculus. 2000