Maintaining consistency under changes to formal specifications

  • Kelvin J. Ross
  • Peter A. Lindsay
Part of the Lecture Notes in Computer Science book series (LNCS, volume 670)


Configuration Management is an integral requirement of the Software Engineering process. This paper outlines an approach to Configuration Management specifically tailored to support formal development of software. A model of VDM developments is defined in which each development is provided as a configuration of its low level components, such as operation definitions and formal proofs. Consistency checking is defined on this model to determine if verification criteria required by the methodology have been carried out. The basis of the consistency checking is determined from relationships between components of the configurations provided by the development tools and the developers themselves. A small VDM case study to which a change is applied is provided to illustrate the model and the support envisaged through the use of consistency checking.


formal methods VDM configuration management change control verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BHS79]
    E. H. Bersoff, V. D. Henderson, and S. G. Siegel. Software Configuration Management: A Tutorial. IEEE Computer, 12(1), Jan 1979.Google Scholar
  2. [Dar91]
    S. Dart. Concepts in Configuration Management Systems. In Proceedings of the Third International Software Configuration Management Workshop, pages 1–18, Trondheim, Norway, June 1991. IEEE CS, ACM Press.Google Scholar
  3. [FMB89]
    P. K. D. Froome, B. Q. Monahan, and R. E. Bloomfield. SpecBox — a checker for VDM Specifications. In Proceedings of Second International Conference on Software Engineering for Real Time Systems, Cirencester, UK, 1989. IEE 1989.Google Scholar
  4. [JJLM91]
    C. B. Jones, K. D. Jones, P. A. Lindsay, and R. D. Moore. Mural: A Formal Development Support System. Springer-Verlag, London, 1991.Google Scholar
  5. [Jon90]
    C. B. Jones. Systematic Software Development using VDM. Prentice Hall International, second edition, 1990.Google Scholar
  6. [Laf90]
    C. Lafontaine. Formalization of the VDM reification in the DEVA metacalculus. Programming Concepts and Methods, pages 333–368, 1990.Google Scholar
  7. [RL93]
    K. Ross and P. Lindsay. Maintaining consistency under changes to formal specifications: an extended case study. Technical Report No. 93-3, Software Verification Research Centre, Dept. of Comp. Sci., University of Queensland, 1993.Google Scholar
  8. [Soc87]
    IEEE Computer Society. IEEE Guide to Software Configuration Management. ANSI/IEEE Std 1042-1987, 1987.Google Scholar
  9. [Soc90]
    IEEE Computer Society. IEEE Standard for Software Configuration Management Plans. IEEE Std 828-1990, 1990.Google Scholar
  10. [Wei90]
    Douglas Weibe. Generic Software Configuration Management: Theory and Design. PhD thesis, Department of Computer Science, University of Washington, Seattle, WA 98195, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Kelvin J. Ross
    • 1
  • Peter A. Lindsay
    • 1
  1. 1.Software Verification Research Centre Department of Computer ScienceUniversity of QueenslandSt LuciaAustralia

Personalised recommendations