Book contents
- Frontmatter
- Contents
- Foreword
- Preface
- 1 Introduction
- 2 Constructing a Model
- 3 VDMTools Lite
- 4 Describing System Properties Using Logical Expressions
- 5 The Elements of a Formal Model
- 6 Sets
- 7 Sequences
- 8 Mappings
- 9 Recursive Structures
- 10 Validating Models
- 11 State-Based Modelling
- 12 Large-Scale Modelling
- 13 Using VDM in Practice
- Appendix A Language Guide
- Appendix B Solutions to Exercises
- Bibliography
- Subject Index
- Definitions Index
13 - Using VDM in Practice
Published online by Cambridge University Press: 03 February 2010
- Frontmatter
- Contents
- Foreword
- Preface
- 1 Introduction
- 2 Constructing a Model
- 3 VDMTools Lite
- 4 Describing System Properties Using Logical Expressions
- 5 The Elements of a Formal Model
- 6 Sets
- 7 Sequences
- 8 Mappings
- 9 Recursive Structures
- 10 Validating Models
- 11 State-Based Modelling
- 12 Large-Scale Modelling
- 13 Using VDM in Practice
- Appendix A Language Guide
- Appendix B Solutions to Exercises
- Bibliography
- Subject Index
- Definitions Index
Summary
Aims
This final chapter concerns the use of VDM in industrial practice. We aim to equip the reader to apply VDM technology cost-effectively in industrial software development processes, and to stay abreast of the state of the art in VDM and formal modelling. We aim to introduce the contribution that formal modelling can make to the tasks that are at the core of commercial development processes. We will illustrate this with several real industrial applications of VDM. Finally, we aim to provide information on the recent extensions to VDM and VDMTools, and how to gain the most from the VDM and formal methods communities.
Introduction
Modelling in a formal language is not a panacea for every problem in system and software development but, if used thoughtfully, it can yield significant benefits. The deciding factor in using VDM technology (the combination of VDM-SL and VDMTools) has to be cost-effectiveness. The cost of developing a system model during the early stages of design should be recouped when the improved understanding of system functionality reduces the reworking required to deal with defects that are uncovered during later activities such as testing and maintenance. In this chapter we discuss a range of software development activities, some of the problems that can arise during their execution and the ways in which the use of VDM can address some of these (Sections 13.2 to 13.4). Some hints on how to start using VDM are presented (Section 13.5). We illustrate the approach by describing recent industrial applications of VDM and its extended forms (Sections 13.6 and 13.7).
- Type
- Chapter
- Information
- Modelling SystemsPractical Tools and Techniques in Software Development, pp. 217 - 234Publisher: Cambridge University PressPrint publication year: 2009