## FME '93: Industrial-Strength Formal Methods: First International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993. ProceedingsJim Woodcock, James C.P. Woodcock, Peter G. Larsen The last few years have borne witness to a remarkable diversity of formal methods, with applications to sequential and concurrent software, to real-time and reactive systems, and to hardware design. In that time, many theoretical problems have been tackled and solved, and many continue to be worked upon. Yet it is by the suitability of their industrial application and the extent of their usage that formal methods will ultimately be judged. This volume presents the proceedings of the first international symposium of Formal Methods Europe, FME'93. The symposium focuses on the application of industrial-strength formal methods. Authors address the difficulties of scaling their techniques up to industrial-sized problems, and their suitability in the workplace, and discuss techniques that are formal (that is, they have a mathematical basis) and that are industrially applicable. The volume has four parts: - Invited lectures, containing a lecture by Cliff B. Jones and a lecture by Antonio Cau and Willem-Paul de Roever; - Industrial usage reports, containing 6 reports; - Papers, containing 32 selected and refereedpapers; - Tool descriptions, containing 11 descriptions. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Reasoning about Interference in an ObjectBased Design Method | 1 |

Using Relative Refinement for Fault Tolerance | 19 |

Specification and Validation of a Security Policy Model | 42 |

Experiences from Applications of RAISE | 52 |

Role of VDM++ in the Development of a RealTime Tracking and Tracing System | 64 |

The Integration of LOTOS with an Object Oriented Development Method | 73 |

An Industrial Experience on LOTOSBased Prototyping for Switching Systems Design | 83 |

Towards an Implementationoriented Specification of TP Protocol in LOTOS | 93 |

Application of Composition Development Method for definition of SYNTHESIS Information Resource Query Language Semantics | 428 |

Verification Tools in the Development of Provably Correct Compilers | 442 |

W A Logic for Z in 2OBJ | 462 |

Some Lessons Learned | 482 |

Conformity Clause for VDMSL | 501 |

Process Instances in LOTOS Simulation | 521 |

Integrating SSADM and Z | 541 |

Maintaining Consistency Under Changes to Formal Specifications | 558 |

A Metalanguage for the Formal Requirement Specification of Reactive Systems | 110 |

The T9000 Virtual Channel Processor | 129 |

Algorithm Refinement with Read and Write Frames | 148 |

a Comparison of the VDM and B Notations | 162 |

A Perspective | 183 |

A Proof Environment for Concurrent Programs | 196 |

A VDM Study of FaultTolerant Stable Storage Towards a Computer Engineering Mathematics | 216 |

Applications of Modal Logic for the Specification of RealTime Systems | 235 |

Industrial Usage | 250 |

Automating the Generation and Sequencing of Test Cases from ModelBased Specifications | 268 |

A Common Execution Model for FDTs | 285 |

Generalizing Abadi Lamports Method to Solve a Problem Posed by A Pmieli | 294 |

RealTime Refinement | 314 |

Different FDTs Confronted with Different ODPViewpoints of the Trader | 332 |

On the Derivation of Executable Database Programs from Formal Specifications | 351 |

A Concurrency Case Study Using RAISE | 367 |

Specifying a SafetyCritical Control System in Z | 388 |

An Overview of the SPRINT Method | 403 |

An EVES Data Abstraction Example | 578 |

the ARA Tool | 597 |

Integrating SART with LOTOS | 617 |

Symbolic Model Checking for Distributed RealTime Systems | 632 |

Adding Specification Constructors to the Refinement Calculus | 652 |

Selling Formal Methods to Industry | 671 |

ProofPower Mural | 679 |

IPTES Toolset The CentaurVDM environment | 680 |

IFAD VDMSL Toolbox DSTfuzz | 681 |

The LOTOS Toolbox Centaur | 682 |

DisCo The BoyerMoore Theorem Prover | 683 |

BTOOLKIT Pet Dingo | 684 |

SpecBox Raise | 685 |

ExSpect CADiZ | 686 |

DesignCPN PVS | 687 |

TAV FDR | 688 |

ForMooZ | 689 |

### Other editions - View all

### Common terms and phrases

abstract algebra algorithm analysis application axioms behaviour buffer checking compiler components Computer Science concurrent condition conformity clause constraints constructs correct DBPL defined definition denotes described detection layer entity environment equivalence error event example execution history expression faults finite formal methods formal specification formal verification formula function implementation input instance interaction interface invariant Logic Programming LOTOS machine mathematical model checking module node notation operation output physical disk possible postcondition predicate problem Proc programming language proof obligations properties protocol prove RAISE Specification Language real-time refinement calculus relation requirements rewrite rules SA/RT schema semantics sequence software development Software Engineering specification language specification statements Springer-Verlag SPRINT SSADM standard step structure syntax tactic techniques temporal logic terminal theorem prover theory tion transformation transition validation variables VDM-SL verification Z notation