عنوان

Proof in VDM

3540761861

9783540761860

b555735

Proof in VDM

[Book]

Juan C. Bicarregui (ed.). Case studies.

London

Springer

1998

xvi, 228 pages : illustrations.

Formal approaches in computing and information technology (FACIT)

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.

Automatisches Beweisverfahren.

Isabelle

VDM.

Juan C. Bicarregui (ed.). Case studies.

[Book]

Y