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