Kevin Lano

The B Language and Method (eBook, PDF)

A Guide to Practical Formal Development

• Format: PDF

Produktbeschreibung

B is one of the few formal methods which has robust, commercially-available tool support for the entire development lifecycle from specification through to code generation. This volume provides a comprehensive introduction to the B Abstract Machine Notation, and to how it can be used to support formal specification and development of high integrity systems. A strong emphasis is placed on the use of B in the context of existing software development methods, including object-oriented analysis and design. The text includes a large number of worked examples, graduated exercises in B AMN specification and development (all of which have been class-tested), two extended case studies of the development process, and an appendix of proof techniques suitable for B. Based on material which has been used to teach B at postgraduate and undergraduate level, this volume will provide invaluable reading a wide range of people, including students, project technical managers and workers, and researchers with an interest in methods integration and B semantics.

---

Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.

Produktdetails

• Verlag: Springer London
• Seitenzahl: 232
• Erscheinungstermin: 6. Dezember 2012
• Englisch
• ISBN-13: 9781447114949
• Artikelnr.: 44000684

Inhaltsangabe

1 Introduction.- 1.1 Formal Methods.- 1.2 The History of B.- 1.3 The Relationship of B to Other Formal Methods.- 1.4 Summary.- 2 The Foundations of B AMN.- 2.1 Mathematical Notation.- 2.2 Defining Operations.- 2.3 Abstract Machines.- 2.4 Machine Composition Mechanisms.- 2.5 Refinement.- 2.6 Implementation.- 2.7 Summary.- 2.8 Exercises 1.- 3 Analysis and Specification.- 3.1 Requirements Analysis.- 3.2 Specification Development.- 3.3 Animation.- 3.4 Proof of Internal Consistency Obligations.- 3.5 Ship Loading Case Study - Specification.- 3.6 Renaming.- 3.7 Aggregation.- 3.8 Summary.- 3.9 Exercises 2.- 4 Design and Implementation.- 4.1 The Layered Development Paradigm.- 4.2 Refinement Examples.- 4.3 Proofs of Refinement.- 4.4 Decomposing Implementations.- 4.5 Ship Loading Case Study - Implementation.- 4.6 Summary.- 4.7 Exercises 3.- 5 Case Studies.- 5.1 Personnel System Development.- 5.2 Mine Pump Control.- 5.3 Vending Machine.- 6 Conclusions.- A Exercise Solutions.- A.1 Exercises 1.- A.2 Exercises 2.- A.3 Exercises 3.- B Properties of Weakest Preconditions.- B.1 Termination and Feasibility.- B.2 Set-theoretic Semantics.- B.3 Refinement.- B.4 Well-formedness Obligations.- B.5 Normal Forms.- B.6 Rules for ?.- B.7 Definition of :=.- C Proof Techniques.