Издательство Springer, 1997, -288 pp.
Formal methods in computer science aim at a scientific foundation on which methods and tools for practical system construction can be based. Practice requires methods for the specification of software systems, tools for checking specifications for syntactic consistency, and support for generation of code from specifications, as well as tools for proving the correctness of manually produced code with respect to the specification. Unfortunately, the practical relevance of many publications on formal methods is limited.
On the other hand, many methods and tools used in practice nowadays do not make use of the current status in computer science research. They are lacking clear concepts, not to speak of a precise definition based on formal techniques. Therefore, there is a need for research aiming at methods that are usable in practice and theoretically founded, in order to provide a basis for powerful tools in software engineering.
In this book Hussmann builds a bridge between the "pragmatic" methods for design of information systems and the formal mathematical background, by giving a formal definition for the method SSADM within the algebraic specification language SPECTRUM. SSADM, a British standard method belonging to the socalled structured methods, serves here as an example. Although SSADM has its methodical deficiencies, the example is well chosen since it is practically relevant. Moreover, it is well suited to demonstrate the power of formal techniques since it is sufficiently complex.
The book gives a complete formal definition for SSADM. This shows that such an approach is not only a theoretical possibility but is also feasible for methods of practical relevance. This is made possible by the usage of clear structuring concepts to build up the formal definition.
The formal foundation of SSADM is more than an example. It is presented in a way that can be seen as a general pattern according to which other software engineering methods also can be defined, in particular the modem object-oriented methods. Our wish for this book is that it encourages other scientists to apply theoretical foundations of computer science to practical problems of software development in a similarly thorough way. Thus the importance of this book goes beyond SSADM and SPECTRUM.
Introduction
Terminology
SSADM - A Pragmatic Requirements Engineering Method
SPECTRUM - A Formal Specification Framework
Alternative Ways to an Integration of SSADM and SPECTRUM
A Semantic Reference Specification for SSADM
The SSADM Technique "Logical Data Modelling"
The SSADM Technique "Entity-Event Modelling"