| Object-oriented design methods are commonplace in computing systems development, but are often dismissed as 'boxes & arrows'. If systems developers are to gain full advantage from such methods, they should be able to achieve designs that are not merely the subject of heated argument, but can be improved by careful, rigorous & machine-supported analysis. This book describes an object-oriented design approach that combines the benefits of abstract modelling with the analytic power of formal methods, to give designs that can be rigorously validated & assured with automated support. Aimed at software architects, designers & developers as well as computer scientists, no prior knowledge of formal methods is assumed. The elements of functional modelling are introduced using numerous examples & exercises, industrial case studies & experience reports. Industry-strength tools support the text. Go to www.vdmbook.com to download free-of-charge VDMTools Lite, which gives the possibility to try out examples from the book
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 computingsystems. 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. |
