Program development by refinement. Case studies using the B method
[The articles of this volume will not be indexed individually.] The B method is an approach for the development of highly trusted software. It uses standard first-order predicate logic, a rich collection of data types and it supports grouping of operations and state variables in moduls called abstract machines. This book is a collection of case studies in program refinement using the B Method. Part 1 includes an introduction to the B Method and the development of information systems. Chapter 1. Introduction to the B Method (Ken A. Robinson). This chapter introduces the basic concepts of the B Method, substitutions, statements, refinement and implementation machines, etc. The use of these is illustrated by a series of examples. Chapter 2. Container Station (Elena Troubitsyna). Starting with precise task description a development of an information system for container station bookkeeping is presented. Performing a number of refinement steps a final implementation is obtained which is translatable to program code. Chapter 3. Minimum Spanning Tree (Ranan Fraer). In this interesting chapter a complete formal development of Kruskal's algorithm for solving the minimum spanning tree problem is presented. Chapter 4. The B Bank (Martin Büchi). A simple banking application with cashier and automated teller machine functionality is developed. An object-oriented model is used as an aid during analysis, which is translated to a B machine which specifies the key functionality. Part 2 is devoted to the development of distributed systems and process control systems. Chapter 5. Parallel Programming with the B Method (Michael Butler and Marina Waldén). In this chapter a brief introduction to active systems is presented and described how they can be embedded in the B Method. Chapter 6. Production Cell (Emil Sekerinski). This chapter illustrates an approach for developing a control program for a discrete control system by the example of a production cell consisting of several interacting machines. Chapter 7. Distributed load Balancing (Marina Waldén). A load balancing algorithm for a process network is developed in this chapter. The algorithm is refined into a distributed action system using the superposition refinement method. It is shown how this refinement method is formalized within the B Method. Chapter 8. Distributed Electronic Mail System (Michael Butler). In this chapter the design of an electronic mail system on a store-and-forward network is presented. The design starts with the abstract specification as a single machine with a simple state structure. Subsequent refinements involve the introduction of data structures, the parallel decomposition of the system into subsystems representing the agents at each node in the network and the direct communications links in network. Overall, this interesting book is written in a clear style presupposing a very good familiarity with abstract machine notation, the B Method and with ideas of program development by using abstract machines. In my view it lacks some discussion about a transformation from implementation obtained by B Method to program written in some other programming language (for example Visual C++). Reader who are not familiar with the B Method may only guess how described approach may be used in a practical program development. Moreover, his hesitation is strengthened if he reads in foreword (by David Lorge Parnas): ``Although the general idea of designing by refinement was proposed more than 30 years ago, none of the industrial systems that I have examined was produced by such a process.\dots Refinement does not seem to have worked in practice. Nevertheless I can recommend the book to anyone who well knows the B Method and finds it usefull.
- Verifying minimum spanning tree algorithms with Stone relation algebras
- B: Towards zero defect software
- Dynamic logic with binders and its application to the development of reactive systems
- Interpreting the B-method in the refinement calculus
- Reactive system refinement of distributed systems in B
- Action systems in incremental and aspect-oriented modeling
- Query-driven verification of data integration in the RDF data model
- Verification-Led Smart Contracts
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
This page was built for publication: Program development by refinement. Case studies using the B method
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4229232)
