Analysis and Specification

Abstract

In this chapter we will examine each of the life cycle stages of B AMN development from requirements analysis through to the creation of a complete specification. A number of case studies and examples are used to illustrate these stages and the choices that can be made in expressing the semantics of a system using B. We will emphasise a particular approach using translation from diagrammatic models to inspire the choice of features of the formal specification, however it is quite feasible to directly write formal specifications without prior analysis or such a translation process (people have been writing Z or VDM specifications this way for years). For complex systems a loss of quality is nevertheless likely to result from omitting analysis.