Software Specification Methods

Henri Habrias, Marc Frappier, Henri Habrias, Marc Frappier

• Publisher: Wiley-ISTE
• Year: 2013
• Print ISBN: 9781905209347
• eBook ISBN: 9781118613948
• Edition: 1
• Topic: Ciencia de la computación
• Subtopic: Desarrollo de software

This title provides a clear overview of the main methods, and has a practical focus that allows the reader to apply their knowledge to real-life situations. The following are just some of the techniques covered: UML, Z, TLA+, SAZ, B, OMT, VHDL, Estelle, SDL and LOTOS.

Part I

State-Based Approaches

Chapter 1

Z

Jonathan P. BOWEN

Oui, l’oeuvre sort plus belle

D’une forme au travail

Rebelle,

Vers, marbre, onyx, émail.

[Yes, the work comes out more beautiful from a material that resists the process, verse, marble, onyx, or enamel.]

– Théophile Gautier (1811–1872) L’Art

1.1 Overview of the Z notation

Z (pronounced ‘zed’) is a formal specification notation based on set theory and first order predicate logic. The mathematical notation is supported by a library of operators known as the ‘Z toolkit’, which is largely formally defined within the Z notation itself [ISO 02, SPI 01]. The operators have a large number of algebraic laws which aid in the reasoning about Z specification. As well as the mathematical notation, there is a ‘schema’ notation to aid in the structuring of the mathematics for large specification by packaging the mathematical notation into boxes that may be used and combined subsequently.

There are many Z textbooks, some of which are available online (see for example, [BOW 03, JAC 97, LIG 00, WOO 96]). A widely used reference book is also accessible online [SPI 01]. Z has subsequently undergone a lengthy international ISO standardization process culminating in 2002 [ISO 02], which could help in the development of further tools to support the notation. In particular, an open source Community Z Tools (CZT) initiative is underway, based around XML [MAL 05]. Z has been extended in a number of ways, especially with object-orienting features (e.g., Object-Z [SMI 00]). The theoretical basis of Z has been explored extensively (e.g., see [HEN 03]). A range of case studies and a Z glossary may be found in [BOW 03].

1.1.1 The process of producing a Z specification

Z is typically used in a modelling style [BOW 04] in which an abstract state is included, containing enough information to describe changes in state that may be performed by a number of operations on the system. Each of the operations defines a relation between a before and after version of the state. The state may contain invariants which are predicates relating the various components in the abstract state which should always apply regardless of the current state of the system.

An initial state is defined as a special case of the more general abstract state, with the addition of extra constraining predicates. The description of the system is then modeled by this initial state, followed by an arbitrary interleaving of the operations in any order, only limited by any preconditions imposed by individual operations.

Often operations are designed to be total (i.e., with a precondition of true) so that they can be applied in any situation. This is especially useful in maintenance of the implemented operations (which could typically be procedure calls, for example) since preconditions are not explicitly obvious in a program implementation and a maintainer unaware of such restrictions may be tempted to use the operation in an inappropriate situation.

In the case of Z, a good place to start the specification is by positing a possible abstract state to model the system. Inevitably this will have to be changed in the course of producing the rest of the specification (except in trivial cases), but that is part of the learning process by which knowledge and understanding of the system is gained.

Next, some operations which may be performed on the system should be considered. Initially only the result of successful operations which perform the desired result with no problems should be formulated. The abstract state should be modified as required if some important aspect cannot be adequately modeled without it, always checking for the possible effect on other operations.

As the specification evolves, given sets and useful axiomatic or generic definitions can be assumed, then formally defined and added at the beginning of the specification. Errors reports in the case of unsuccessful operations should be considered and added. Some of these will normally be common across several operations in a specification of any size.

In practical specifications, it will be found that parts of the specification are repeated across groups of operations. It is often worthwhile factoring out these parts, presenting and explaining their purpose once, and then using them subsequently. This will considerably reduce the size of most large specifications and make their assimilation easier for the reader.

Total operations are normally formulated typically as a disjunction of the successful and, if required, a number of error cases. An appropriate error indication, normally as some form of output, is normally included depending on the requirements.

Finally (perhaps surprisingly) the initial state should be considered as a special case of the abstract state. Often the contents of much of the state are most easily considered to be empty or to have some fixed value at the start of the life of the system, but may be more loosely specified if the exact value is unimportant.

During the production of the specification, questions will inevitably be raised. These should be discussed within the design team, with other colleagues, or with the customer as appropriate, normally in that order, to resolve the issues. In the next section of this chapter, a Z specification is presented with some of these questions interspersed with the formal Z specification. Informal description of the formal specification is also included. This should be designed to reinforce the concepts presented in the Z specification, especially in relating it to the real world.

In a finished and polished Z specification, the informal annotation should normally be about the same length as the formal description. As a rule of thumb, it is a good idea to attempt to describe each line of predicate in Z schema boxes with a matching sentence of text written in a natural style. Ideally the informal part of the specification should be meaningful on its own, even if the formal part is removed. In fact this could be useful if the description is to be presented to a customer who may be unable to assimilate the Z specification itself.

1.2 Analysis and specification of case 1

Most specifications, formal or otherwise, are presented as a fait accompli after the specification has be...

Table of contents

• Cover
• Title Page
• Copyright
• Dedication
• Preface
• List of Contributors
• Part I: State-Based Approaches
• Part II: Event-Based Approaches
• Part III: Other Formal Approaches
• Part IV: Comparison and Glossary
• Index