This book constitutes the refereed proceedings of the Second International Conference of B and Z Users, ZB 2002, held in Grenoble, France in January 2002. The 24 papers presented together with three invited contributions were carefully reviewed and selected for inclusion in the book. The book documents the recent advances for the Z formal specification notion and for the B method; the full scope is covered, ranging from foundational and theoretical issues to advanced applications, tools, and case studies.
Author(s): Eric Hehner, Ioannis T. Kassios (auth.), Didier Bert, Jonathan P. Bowen, Martin C. Henson, Ken Robinson (eds.)
Series: Lecture Notes in Computer Science 2272
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2002
Language: English
Pages: 541
Tags: Software Engineering; Mathematical Logic and Formal Languages
Theories, Implementations, and Transformations....Pages 1-21
Incremental Proof of the Producer/Consumer Property for the PCI Protocol....Pages 22-41
Controlling Control Systems: An Application of Evolving Retrenchment....Pages 42-61
Checking Z Data Refinements Using an Animation Tool....Pages 62-81
Encoding Object-Z in Isabelle/HOL....Pages 82-99
Characters + Mark-up = Z Lexis....Pages 100-119
Extraction of Abstraction Invariants for Data Refinement....Pages 120-139
An Approach to Combining B and Alloy....Pages 140-161
Software Construction by Stepwise Feature Introduction....Pages 162-183
The Semantics of Circus ....Pages 184-203
Handling Inconsistencies in Z Using Quasi-Classical Logic....Pages 204-225
Loose Specification and Refinement in Z....Pages 226-241
On Using Conditional Definitions in Formal Theories....Pages 242-269
A Theory of Generalised Substitutions....Pages 270-290
Reinforced Condition/Decision Coverage (RC/DC): A New Criterion for Software Testing....Pages 291-308
A Comparison of the BTT and TTF Test-Generation Methods....Pages 309-329
A Formal Analysis of the CORBA Security Service....Pages 330-349
Type Synthesis in B and the Translation of B to PVS....Pages 350-369
“Higher-Order” Mathematics in B....Pages 370-393
ABS Project: Merging the Best Practices in Software Design from Railway and Aircraft Industries....Pages 394-395
Generalised Substitution Language and Differentials....Pages 396-415
Communicating B Machines....Pages 416-435
Synchronized Parallel Composition of Event Systems in B....Pages 436-457
Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study....Pages 458-476
Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions....Pages 477-496
A Formal Model of the UML Metamodel: The UML State Machine and Its Integrity Constraints....Pages 497-516
Coming and Going from UML to B: A Proposal to Support Traceability in Rigorous IS Development....Pages 517-534
