Preface
Object-oriented design is common in computing systems development. There is a plethora of techniques and an abundance of texts on the subject. Why, then, a book on validated designs for object-oriented systems? Our experience with specification, modelling and analysis techniques over the last decade tells us that object-oriented design is much more than mere “boxes and arrows.” Systems developers should be able to combine techniques and tools to achieve designs that are not merely the subject
of heated argument but can be improved by careful, rigorous and machine-supported analysis. This book describes an approach to the design of object-oriented systems which combines the benefits of abstract modelling with the analytic power of formal
methods to give designs that can be rigorously validated and assured with automated support.
System modelling has a valuable contribution to make in the development of computing systems. It encourages abstract, systematic and comprehensive consideration of system aspects, including the description of functionality, interactions with the environment and temporal behaviour. The rising level of interest in modelling is evidenced by the central role being taken by model-driven development approaches within the software engineering communities, such as the model-driven architecture work by the Object Management Group. Formal methods can bring further tangible benefits to systems and software development, including objectivity and rigour of analysis, without compromising abstraction. However, these benefits can only be realised in practice if formal techniques are carefully targeted. In particular, formal techniques cannot be applied in isolation but must work alongside other analysis and design tools. The successful application of these techniques is regularly reported. This book stands in the tradition of “Lightweight” formal methods. Its aim is to equip readers with the ability to take advantage of formal modelling techniques without necessarily having to deploy the whole panoply of formal methods. We show how a formal notation (VDM++) can be used to complement and enhance object-oriented class models, with the engineer free to move between the class structure view and the functional view in VDM++. The approach shows how formal techniques can be used to take practitioners on from where they are, rather than requiring a radical shake-up of existing practice.