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.
Author(s): C. B. Jones (auth.), James C. P. Woodcock, Peter G. Larsen (eds.)
Series: Lecture Notes in Computer Science 670
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1993
Language: English
Pages: 695
Tags: Programming Techniques; Software Engineering; Logics and Meanings of Programs; Business Information Systems
Reasoning about interference in an object-based design method....Pages 1-18
Using relative refinement for fault tolerance....Pages 19-41
Specification and validation of a security policy model....Pages 42-51
Experiences from applications of RAISE....Pages 52-63
Role of VDM(++) in the development of a real-time tracking and tracing system....Pages 64-72
The integration of LOTOS with an object oriented development method....Pages 73-82
An industrial experience on LOTOS-based prototyping for switching systems design....Pages 83-92
Towards an implementation-oriented specification of TP protocol in LOTOS....Pages 93-109
A metalanguage for the formal requirement specification of reactive systems....Pages 110-128
Model checking in practice....Pages 129-147
Algorithm refinement with read and write frames....Pages 148-161
Invariants, frames and postconditions: a comparison of the VDM and B notations....Pages 162-182
The industrial take-up of formal methods in safety-critical and other areas: A perspective....Pages 183-195
A proof environment for concurrent programs....Pages 196-215
A VDM ♣ study of Fault-Tolerant stable storage — Towards a computer engineering mathematics....Pages 216-234
Applications of modal logic for the specification of real-time systems....Pages 235-249
Formal methods reality check: Industrial usage....Pages 250-267
Automating the generation and sequencing of test cases from model-based specifications....Pages 268-284
The parallel abstract machine: A common execution model for FDTs....Pages 285-293
Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli....Pages 294-313
Real-time refinement....Pages 314-331
Different FDT's confronted with different ODP-viewpoints of the trader....Pages 332-350
On the derivation of executable database programs from formal specifications....Pages 351-366
A concurrency case study using RAISE....Pages 367-387
Specifying a safety-critical control system in Z....Pages 388-402
An overview of the SPRINT method....Pages 403-427
Application of composition development method for definition of SYNTHESIS information resource query language semantics....Pages 428-441
Verification tools in the development of provably correct compilers....Pages 442-461
Encoding $$\mathcal{W}$$ : A Logic for Z in 2OBJ....Pages 462-481
Formal verification for fault-tolerant architectures: Some lessons learned....Pages 482-500
Conformity clause for VDM-SL....Pages 501-520
Process instances in LOTOS simulation....Pages 521-540
The SAZ project: Integrating SSADM and Z....Pages 541-557
Maintaining consistency under changes to formal specifications....Pages 558-577
An EVES data abstraction example....Pages 578-596
Putting advanced reachability analysis techniques together: The “ARA” tool....Pages 597-616
Integrating SA/RT with LOTOS....Pages 617-631
Symbolic model checking for distributed real-time systems....Pages 632-651
Adding specification constructors to the refinement calculus....Pages 652-670
Selling formal methods to industry....Pages 671-678
Tool Descriptions....Pages 679-689
