FME '93: Industrial-Strength Formal Methods

1. Front Matter

   PDF

2. Reasoning about interference in an object-based design method

   • C. B. Jones

   Pages 1-18

3. Using relative refinement for fault tolerance

   • Antonio Cau, Willem-Paul de Roever

   Pages 19-41

4. Specification and validation of a security policy model

   • Tony Boswell

   Pages 42-51

5. Experiences from applications of RAISE

   • Bent Dandanell, Jesper Gørtz, Jan Storbank Pedersen, Eld Zierau

   Pages 52-63

6. Role of VDM(++) in the development of a real-time tracking and tracing system

   • E. H. Dürr, E. M. Dusink

   Pages 64-72

7. The integration of LOTOS with an object oriented development method

   • Mikael Hedlund

   Pages 73-82

8. An industrial experience on LOTOS-based prototyping for switching systems design

   • Gonzalo León, Juan C. Yelmo, Carlos Sánchez, F. Javier Carrasco, Juan J. Gil

   Pages 83-92

9. Towards an implementation-oriented specification of TP protocol in LOTOS

   • Ing Widya, Gert-Jan van der Heijden

   Pages 93-109

10. A metalanguage for the formal requirement specification of reactive systems

    • Egidio Astesiano, Gianna Reggio

    Pages 110-128

11. Model checking in practice

    • Geoff Barrett

    Pages 129-147

12. Algorithm refinement with read and write frames

    • Juan Bicarregui

    Pages 148-161

13. Invariants, frames and postconditions: a comparison of the VDM and B notations

    • Juan Bicarregui, Brian Ritchie

    Pages 162-182

14. The industrial take-up of formal methods in safety-critical and other areas: A perspective

    • Jonathan Bowen, Victoria Stavridou

    Pages 183-195

15. A proof environment for concurrent programs

    • Naïma Brown, Dominique Mery

    Pages 196-215

16. A VDM ^♣ study of Fault-Tolerant stable storage — Towards a computer engineering mathematics

    • Andrew Butterfield

    Pages 216-234

17. Applications of modal logic for the specification of real-time systems

    • Liang Chen, Alistair Munro

    Pages 235-249

18. Formal methods reality check: Industrial usage

    • Dan Craigen, Susan Gerhart, Ted Ralston

    Pages 250-267

19. Automating the generation and sequencing of test cases from model-based specifications

    • Jeremy Dick, Alain Faivre

    Pages 268-284

20. The parallel abstract machine: A common execution model for FDTs

    • Guillaume Doumenc, Jean-Francois Monin

    Pages 285-293

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.

• Formal Methods
• Formale Methoden
• Object-Orientation
• Petri Nets
• Petri-Netze
• Refinement Calculus
• Vienna Development Method (VDM)
• design
• formal method
• hardware
• real-time

Policies and ethics