| ISBN |
9781447115328 |
| 기타 표준번호 |
10.1007/978-1-4471-1532-8 |
| 청구기호 |
QA267-268.5 |
| 다른형태 서명 |
With contributions by numerous experts.
|
| 형태사항 |
XV, 226 p. online resource.
|
| 언어 |
English |
| 내용 |
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.5 Issues Raised by the Study -- 1.6 Conclusions -- 1.7 Bibliography -- 2 The Ammunition Control System -- 2.1 Introduction -- 2.2 The Specification -- 2.3 Satisfiability of ADD-OBJECT -- 2.4 Modifying the Specification -- 2.5 Discussion -- 2.6 Bibliography -- 2.7 Auxiliary Results -- 3 Specification and Validation of a Network Security Policy Model -- 3.1 Introduction -- 3.2 The Data Model -- 3.3 The System State -- 3.4 Operations Modelling the SEFs -- 3.5 The Proofs -- 3.6 Conclusions -- 3.7 Bibliography -- 4 The Specification and Proof of an EXPRESS to SQL “Compiler” -- 4.1 STEP and EXPRESS -- 4.2 An Outline of EXPRESS -- 4.3 The Abstract EXPRESS Database -- 4.4 A Relational Database -- 4.5 A Concrete EXPRESS Database -- 4.6 A Refinement Proof -- 4.7 General Experiences and Conclusions -- 4.8 Bibliography -- 5 Shared Memory Synchronization -- 5.1 Introduction -- 5.2 Formal Definitions -- 5.3 The VDM Specification of the Definitions -- 5.4 A Theory for Shared Memory Synchronization -- 5.5 Discussion -- 5.6 Related Work -- 5.7 Appendix A. A Formal Theory for Relations -- 5.8 Appendix B. Some Rules Used in the Proof -- 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.4 A Specification Example: MSMIE -- 6.5 Representing Refinement -- 6.6 Discussion -- 6.7 Conclusion -- 6.8 Bibliography -- 7 Supporting Proof in VDM-SL using Isabelle -- 7.1 Introduction -- 7.2 Overview of Approach -- 7.3 Syntax -- 7.4 Proof System of VDM-LPF -- 7.5 Proof Tactics -- 7.6 Transformations -- 7.7 Generating Axioms: An Example -- 7.8 Future Work -- 7.9 Conclusion -- 7.10 Bibliography -- 7.11 VDM-SL Syntax in Isabelle.
|
| 주제 |
Machine theory.
Software engineering.
Compilers (Computer programs).
Formal Languages and Automata Theory.
Software Engineering.
Compilers and Interpreters.
|
| 보유판 및 특별호 저록 |
Springer Nature eBook
Printed edition: 9783540761860
Printed edition: 9781447115335
|
| QR CODE |
|
