Zb 2002: Formal Specification and Development in Z and B: 2nd International Conference of B and Z Users Grenoble, France, January 23-25, 2002, Proceed

ISBN-13: 9783540431664 / Angielski / Miękka / 2002 / 541 str.

D. Bert; J. P. Bowen; M. C. Henson

Opis

This volume 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 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.

Spis treści

Theories, Implementations, and Transformations.- Incremental Proof of the Producer/Consumer Property for the PCI Protocol.- Controlling Control Systems: An Application of Evolving Retrenchment.- Checking Z Data Refinements Using an Animation Tool.- Encoding Object-Z in Isabelle/HOL.- Characters + Mark-up = Z Lexis.- Extraction of Abstraction Invariants for Data Refinement.- An Approach to Combining B and Alloy.- Software Construction by Stepwise Feature Introduction.- The Semantics of Circus.- Handling Inconsistencies in Z Using Quasi-Classical Logic.- Loose Specification and Refinement in Z.- On Using Conditional Definitions in Formal Theories.- A Theory of Generalised Substitutions.- Reinforced Condition/Decision Coverage (RC/DC): A New Criterion for Software Testing.- A Comparison of the BTT and TTF Test-Generation Methods.- A Formal Analysis of the CORBA Security Service.- Type Synthesis in B and the Translation of B to PVS.- “Higher-Order” Mathematics in B.- ABS Project: Merging the Best Practices in Software Design from Railway and Aircraft Industries.- Generalised Substitution Language and Differentials.- Communicating B Machines.- Synchronized Parallel Composition of Event Systems in B.- Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study.- Verification of Dynamic Constraints for B Event Systems under Fairness Assumptions.- A Formal Model of the UML Metamodel: The UML State Machine and Its Integrity Constraints.- Coming and Going from UML to B: A Proposal to Support Traceability in Rigorous IS Development.

O autorze

Sir Ken Robinson ist einer der international renommiertesten Trainer, wenn es um die Entwicklung des menschlichen Potenzials geht. Er arbeitete für Regierungen in Europa und Asien, Großkonzerne und einige der bedeutendsten Non-Profit-Organisationen der Welt. Er lebt mit seiner Frau und zwei Kindern in Los Angeles.