Proof in VDM: Case Studies

1. Front Matter

   Pages i-xv

   PDF

2. Proof in the Analysis of a Model of a Tracking System

   • John Fitzgerald, Cliff Jones

   Pages 1-29

3. The Ammunition Control System

   • Paul Mukherjee, John Fitzgerald

   Pages 31-64

4. Specification and Validation of a Network Security Policy Model

   • Peter Lindsay

   Pages 65-93

5. The Specification and Proof of an EXPRESS to SQL “Compiler”

   • Juan Bicarregui, Brian Matthews

   Pages 95-121

6. Shared Memory Synchronization

   • Noemie Slaats, Bart Van Assche, Albert Hoogewijs

   Pages 123-156

7. On the Verification of VDM Specification and Refinement with PVS

   • Sten Agerholm, Juan Bicarregui, Savi Maharaj

   Pages 157-189

8. Supporting Proof in VDM-SL using Isabelle

   • Sten Agerholm, Jacob Frost

   Pages 191-223

9. Back Matter

   Pages 225-226

   PDF

Not so many years ago, it would have been difficult to find more than a handful of examples of the use of formal methods in industry. Today however, the industrial application of formal methods is becoming increasingly common in a variety of application areas, particularly those with a safety, security or financially critical aspects. Furthermore, in situations where a particularly high level of assurance is required, formal proof is broadly accepted as being of value. Perhaps the major benefit of formalisation is that it enables formal symbolic manip­ ulation of elements of a design and hence can provide developers with a variety of analyses which facilitate the detection of faults. Proof is just one of these possible formal activities, others, such as test case generation and animation, have also been shown to be effective bug finders. Proof can be used for both validation and verifi­ cation. Validation of a specification can be achieved by proving formal statements conjectured about the required behaviours of the system. Verification of the cor­ rectness of successive designs can be achieved by proof of a prescribed set of proof obligations generated from the specifications.

• Erfüllbarkeitsproblem der Aussagenlogik
• Isabelle
• Rack
• SQL
• compiler
• development
• formal methods
• formal specification
• logic
• modeling
• proof theory
• theorem proving
• validation
• verification

• Department of Computing, Imperial College of Science, Technology and Medicine, London, UK

  J. C. Bicarregui

• Computing and Information Systems Department, Rutherford Appleton Laboratory, Chilton, Didcot, Oxfordshire, UK

  J. C. Bicarregui

Policies and ethics