Proof in VDM: Case Studies
By: edited by J.C. Bicarregui
Series: Formal Approaches to Computing and Information Technology (FACIT); Formal Approaches to Computing and Information Technology (FACIT)
Publisher: Springer London
Published: 1998
Place of publication: London
Language: eng
Format: [electronic resource] /
Number of pages: 226
ISBN-13: 9781447115328
Other titles: With contributions by numerous experts
Description: This volume provides an invaluable companion to Proof in VDM: A Practitioner's Guide. Using the proof theory presented in that volume, it examines a variety of realistic case studies which illustrate different aspects of the use of proof in formal development. Rather than concentrating on the construction of formal specifications (like most work in this area), it devotes two chapters to validation using proof, describing how proofs in VDM can be constructed via instantiations of the PVS and Isabelle theorem provers. Proof in VDM: Case Studies will provide invaluable reference material for practitioners of formal methods who need to construct proofs, students requiring a detailed introduction to the practicalities of proof, and researchers interested in the role of theorem proving in formal development and relevant tool support.
Table of contents: title: Introduction; title: A Tracking System; title: The Ammunition Control System; title: A Network Security Model; title: An EXPRESS to SQL Compiler; title: Shared Memory Synchronization; title: VDM Proofs in PVS; title: Index.