FME '93: Industrial-Strength Formal Methods: First International Symposium of Formal Methods Europe, Odense, Denmark, April 19-23, 1993. Proceedings

Front Cover
Jim Woodcock, James C.P. Woodcock, Peter G. Larsen
Springer Science & Business Media, 1993 - Business & Economics - 689 pages
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.

Selected pages

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
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information