Specification in B : an introduction using the B toolkit / Kevin Lano, Howard Haughton.

Format:

Book

Author/Creator:

Lano, K.

Contributor:

Haughton, H.

Language:

English

Subjects (All):

B (Computer program language).

Computer programming.

Physical Description:

1 online resource (256 p.)

Place of Publication:

London : Imperial College Press ; Singapore ; River Edge, NJ : Distributed by World Scientific Pub., c1996.

Language Note:

English

Summary:

This book gives a practical introduction to the B specification language and method, an approach to the development of high-quality software using rigorous CASE techniques.It is suitable for both undergraduate and postgraduate courses, in addition to being an introduction for industrial practitioners. Extensive examples of all development life-cycle stages are given, including animation, proof, design and code generation in C. Two large case studies and exercises with solutions are provided.The authors have extensive experience in teaching B and in its industrial application to high integrity

Contents:

Acknowledgement; Preface; Foreword; Contents; Chapter 1 Abstract Machines; 1.1 Software Development Lifecycles; 1.2 Specification using Abstract Machines; 1.2.1 Mathematical Notation; 1.2.2 Machine Parameters; 1.2.3 Sets; 1.2.4 Constants and Properties; 1.2.5 Variables and Invariants; 1.2.6 Initialisation; 1.2.7 Operation Definitions; 1.3 Semantics of Abstract Machines; 1.3.1 Semantics of Generalised Substitutions; 1.4 Internal Consistency; 1.5 Animation; 1.6. EXERCISES 1; Chapter 2 Constructing Specifications; 2.1 Machine Composition Mechanisms; 2.2 Structuring Mechanisms and Proof

2.3 Translation of Analysis Models2.4 Renaming; 2.5 Exercises 2; Chapter 3 Design and Refinement; 3.1 The Layered Development Paradigm; 3.2 Refinement; 3.3. IMPLEMENTATION; 3.3.1 Examples of Implementation; 3.4 System Construction; 3.5 Implementation Example - Vending Machines; 3.6 Exercises 3; Chapter 4 Proof; 4.1 The B Tool; 4.2 Proof of Internal Consistency Obligations; 4.2.1 Example - ATC Development; 4.2.2 Assertions; 4.2.3 Definitions; 4.3 Proof Listings; 4.4 Animation; 4.5 Refinement Proof; 4.6 Refinement Proof Example - Vending System; 4.7 Exercises 4; Chapter 5 Implementation

5.1 Prototype Generation5.2 Implementing Complex Data; 5.3 Base Generation; 5.4 Coding and Integration; 5.5 Exercises 5; Chapter 6 Case Studies; 6.1 Real-time Communication Protocol; 6.1.1 Specifying the Client; 6.1.2 Specification of the Server; 6.1.3 Buffer Specification; 6.1.4 Timing Properties; 6.1.5 Protocol Specification; 6.1.6 Refinement and Implementation; 6.2 Dependability Evaluation of B AMN Developments; 6.3 Case Study: Radar Track-former System; 6.4 Safety Analysis Techniques for B; 6.4.1 Hazard Analysis; 6.4.2 Verification; 6.4.3 FMECA; 6.5 Timing Analysis of B AMN Specifications

6.6 ConclusionsReferences; Appendix A Exercise Solutions; A.1 Exercises 1; A.2 Exercises 2; A.3 Exercises 3; A.4 Exercises 4; A.5 Exercises 5; Appendix B B AMN and Z; Appendix C B Notation Summary; 1. Predicates; 2. Expressions; 3. Sets; 4. Natural Numbers; 5. Relations; 6. Functions; 7. Sequences; 8. Variables, Variable Lists and Identifiers; 9. Generalised Substitutions; 10. AMN Substitutions; 11. AMN Operations; 12. Machines; 13. Refinements; 14. Implementations; Index

Notes:

Description based upon print version of record.

Includes bibliographical references (p. 183-186) and index.

ISBN:

9781283635622

1283635623

9781848161061

1848161069

OCLC:

813395937