Proof in VDM: Case Studies

ISBN-13: 9783540761860 / Angielski / Miękka / 1998 / 226 str.

J. C. Bicarregui; Juan C. Bicarregui

Opis

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."

Spis treści

1 A Tracking System.- 1.1 Introduction.- 1.2 Context of the Study.- 1.3 A Formal Model of a Tracking System.- 1.4 Analysing the Model with Proof.- 1.4.1 Levels of Rigour in Proof.- 1.4.2 Validation Conjectures.- 1.4.3 Container Packing.- 1.4.4 Safety of Compaction.- 1.5 Issues Raised by the Study.- 1.5.1 Review Cycle.- 1.5.2 Scope of System.- 1.5.3 Tools.- 1.5.4 Genericity and Proofs.- 1.5.5 Testing as a Way of Detecting Problems.- 1.6 Conclusions.- 1.7 Bibliography.- 2 The Ammunition Control System.- 2.1 Introduction.- 2.2 The Specification.- 2.2.1 Explosives Regulations.- 2.2.2 The Model.- 2.2.3 Storing Objects.- 2.3 Satisfiability of ADD-OBJECT.- 2.3.1 Main Satisfiability Proof.- 2.3.2 Formation of the Witness Value.- 2.3.3 Satisfaction of Postcondition.- 2.3.4 Summary.- 2.4 Modifying the Specification.- 2.4.1 Modification to the Specification.- 2.4.2 Proving Equivalence.- 2.5 Discussion.- 2.6 Bibliography.- 2.7 Auxiliary Results.- 3 Specification and Validation of a Network Security Policy Model.- 3.1 Introduction.- 3.1.1 Background and Context.- 3.1.2 Software System Requirements.- 3.1.3 Security Threats and Security Objectives.- 3.1.4 Conceptual Model of the Security Policy.- 3.1.5 The Security Enforcing Functions.- 3.1.6 Specification and Validation of the SPM.- 3.2 The Data Model.- 3.2.1 Partitions.- 3.2.2 Users and User Sessions.- 3.2.3 Classifications.- 3.2.4 Messages.- 3.2.5 Seals.- 3.2.6 Sealing.- 3.2.7 Changing Seals.- 3.2.8 Other Integrity Checks.- 3.2.9 Content Checks.- 3.2.10 Accountability Records.- 3.2.11 The Message Pool.- 3.3 The System State.- 3.4 Operations Modelling the SEFs.- 3.4.1 The Authorise Message Operation.- 3.4.2 The Internal Transfer Operation.- 3.4.3 The Export Operation.- 3.4.4 The Import Operation.- 3.5 The Proofs.- 3.5.1 Consistency Proofs.- 3.5.2 Preservation of the Security Properties.- 3.5.3 Completeness Proofs.- 3.6 Conclusions.- 3.7 Bibliography.- 4 The Specification and Proof of an EXPRESS to SQL “Compiler”.- 4.1 STEP and EXPRESS.- 4.1.1 The Context.- 4.1.2 The Specifications.- 4.1.3 Related Work.- 4.1.4 Overview.- 4.2 An Outline of EXPRESS.- 4.2.1 Entities.- 4.2.2 Other Type Constructors.- 4.2.3 Subtypes.- 4.3 The Abstract EXPRESS Database.- 4.3.1 The EXPRESS and EXPRESS-I Abstract Syntax.- 4.3.2 The State and Operations.- 4.3.3 Reflections on the Abstract Specification.- 4.4 A Relational Database.- 4.4.1 Signature.- 4.4.2 Datatypes.- 4.4.3 The State and Operations.- 4.4.4 Reflections on the Relational Database Specification.- 4.5 A Concrete EXPRESS Database.- 4.6 A Refinement Proof.- 4.6.1 The Retrieve Function.- 4.6.2 The Refinement Proof Obligations.- 4.6.3 Thoughts on the Refinement Proof.- 4.7 General Experiences and Conclusions.- 4.8 Bibliography.- 5 Shared Memory Synchronization.- 5.1 Introduction.- 5.2 Formal Definitions.- 5.2.1 Program Order and Executions.- 5.2.2 Uniprocessor Correctness.- 5.2.3 Result of a Load.- 5.2.4 Synchronization.- 5.2.5 Memory Model.- 5.3 The VDM Specification of the Definitions.- 5.3.1 Operations.- 5.3.2 Useful Functions.- 5.3.3 The Program Order and Executions.- 5.3.4 Memory Order.- 5.3.5 Uniprocessor Correctness.- 5.3.6 The Result of a Load.- 5.3.7 Synchronization Operations.- 5.3.8 Memory Model.- 5.4 A Theory for Shared Memory Synchronization.- 5.4.1 The Formal Language.- 5.4.2 The Set of Inference Rules.- 5.4.3 A Proof.- 5.5 Discussion.- 5.6 Related Work.- 5.7 Appendix A. A Formal Theory for Relations.- 5.7.1 Signature.- 5.7.2 Axioms.- 5.8 Appendix B. Some Rules Used in the Proof.- 5.8.1 Axioms.- 5.8.2 Proof Obligations.- 5.9 Bibliography.- 6 On the Verification of VDM Specification and Refinement with PVS.- 6.1 Introduction.- 6.2 The PVS System.- 6.3 From VDM-SL to the Higher Order Logic of PVS.- 6.3.1 Basic Types, the Product Type and Type Invariants.- 6.3.2 Record Types.- 6.3.3 Sequences, Sets and Maps.- 6.3.4 Union Types.- 6.3.5 Function Definitions.- 6.3.6 Pattern Matching.- 6.3.7 State and Operations.- 6.4 A Specification Example: MSMIE.- 6.4.1 The VDM Specification.- 6.4.2 PVS Translation.- 6.4.3 Typechecking Constraints.- 6.4.4 Some Validation Conditions.- 6.5 Representing Refinement.- 6.5.1 The VDM Specification.- 6.5.2 The PVS Specification.- 6.5.3 The Refinement Relationship.- 6.6 Discussion.- 6.6.1 Using the PVS System.- 6.6.2 Partiality in VDM and PVS.- 6.6.3 Looseness in VDM and PVS.- 6.6.4 Errors in Example Specifications.- 6.7 Conclusion.- 6.8 Bibliography.- 7 Supporting Proof in VDM-SL using Isabelle.- 7.1 Introduction.- 7.2 Overview of Approach.- 7.2.1 Reading of Figure 7.1.- 7.3 Syntax.- 7.4 Proof System of VDM-LPF.- 7.4.1 Proof Rules.- 7.4.2 Combining Natural Deduction and Sequent Style Proof.- 7.5 Proof Tactics.- 7.5.1 Basic Tactics.- 7.5.2 Proof Search Tactics.- 7.5.3 Gateway Example.- 7.6 Transformations.- 7.6.1 Pattern Matching.- 7.6.2 Cases Expressions.- 7.7 Generating Axioms: An Example.- 7.7.1 Type Definitions.- 7.7.2 Function Definitions.- 7.8 Future Work.- 7.9 Conclusion.- 7.10 Bibliography.- 7.11 VDM-SL Syntax in Isabelle.