Overview

Full Product Details

Author:   James C.P. Woodcock ,  Peter G. Larsen
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Edition:   1993 ed.
Volume:   670
Dimensions:   Width: 15.50cm , Height: 3.60cm , Length: 23.30cm
Weight:   2.170kg
ISBN:  

9783540566625

ISBN 10:   3540566627
Pages:   695
Publication Date:   06 April 1993
Audience:   College/higher education ,  Professional and scholarly ,  Postgraduate, Research & Scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of Contents

Reasoning about interference in an object-based design method.- Using relative refinement for fault tolerance.- Specification and validation of a security policy model.- Experiences from applications of RAISE.- Role of VDM(++) in the development of a real-time tracking and tracing system.- The integration of LOTOS with an object oriented development method.- An industrial experience on LOTOS-based prototyping for switching systems design.- Towards an implementation-oriented specification of TP protocol in LOTOS.- A metalanguage for the formal requirement specification of reactive systems.- Model checking in practice.- Algorithm refinement with read and write frames.- Invariants, frames and postconditions: a comparison of the VDM and B notations.- The industrial take-up of formal methods in safety-critical and other areas: A perspective.- A proof environment for concurrent programs.- A VDM ? study of Fault-Tolerant stable storage - Towards a computer engineering mathematics.- Applications of modal logic for the specification of real-time systems.- Formal methods reality check: Industrial usage.- Automating the generation and sequencing of test cases from model-based specifications.- The parallel abstract machine: A common execution model for FDTs.- Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli.- Real-time refinement.- Different FDT's confronted with different ODP-viewpoints of the trader.- On the derivation of executable database programs from formal specifications.- A concurrency case study using RAISE.- Specifying a safety-critical control system in Z.- An overview of the SPRINT method.- Application of composition development method for definition of SYNTHESIS information resource query language semantics.- Verification tools in the development of provably correct compilers.- Encoding $$\mathcal{W}$$ : A Logic for Z in 2OBJ.- Formal verification for fault-tolerant architectures: Some lessons learned.- Conformity clause for VDM-SL.- Process instances in LOTOS simulation.- The SAZ project: Integrating SSADM and Z.- Maintaining consistency under changes to formal specifications.- An EVES data abstraction example.- Putting advanced reachability analysis techniques together: The ARA tool.- Integrating SA/RT with LOTOS.- Symbolic model checking for distributed real-time systems.- Adding specification constructors to the refinement calculus.- Selling formal methods to industry.- Tool Descriptions.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions