Geschäftskunden Kundenprogramme
Vor Ort
Merkzettel Warenkorb
Proof in VDM: Case Studies

Proof in VDM: Case Studies

Aus der Reihe

Fr. 137.00

inkl. gesetzl. MwSt.
Versandkostenfrei
Taschenbuch

Taschenbuch

Fr. 137.00 eBook

eBook

Fr. 125.90

Proof in VDM: Case Studies

Ebenfalls verfügbar als:

Taschenbuch

Taschenbuch

ab Fr. 137.00
eBook

eBook

ab Fr. 125.90

Beschreibung

Details

Einband

Taschenbuch

Erscheinungsdatum

02.03.1998

Herausgeber

Juan C. Bicarregui

Verlag

Springer Berlin

Seitenzahl

226

Beschreibung

Details

Einband

Taschenbuch

Erscheinungsdatum

02.03.1998

Herausgeber

Juan C. Bicarregui

Verlag

Springer Berlin

Seitenzahl

226

Maße (L/B/H)

23.5/15.5/1.3 cm

Gewicht

376 g

Auflage

Softcover reprint of the original 1st ed. 1998

Sprache

Englisch

ISBN

978-3-540-76186-0

Weitere Bände von Formal Approaches to Computing and Information Technology (FACIT)

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen

Informationen zu Bewertungen

Zur Abgabe einer Bewertung ist eine Anmeldung im Konto notwendig. Die Authentizität der Bewertungen wird von uns nicht überprüft. Wir behalten uns vor, Bewertungstexte, die unseren Richtlinien widersprechen, entsprechend zu kürzen oder zu löschen.

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kund*innen durch Ihre Meinung

Erste Bewertung verfassen

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen filtern
  • Proof in VDM: Case Studies
  • 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.