From Analysis to Formal Specification

  • Kevin Lano
Part of the Formal Approaches to Computing and Information Technology FACIT book series (FACIT)


This chapter will describe a systematic process of formalisation of OMT analysis models: data, functional and dynamic, into Z++ and VDM++. The main elements of the data and dynamic models of OMT will be covered in this chapter. The Booch method is also considered [30]. Chapter 7 will cover the OMT notation in greater depth, and also consider the OOA method [271]. The use of this translation process and of specification animation, in providing a common language between the specifier and the client, will be emphasised for its significance in reducing errors in requirements elicitation. It covers the stages of requirements formalisation and specification enhancement described in Chapter 2. Section 3.1 describes the formalisation of object models in Z++ and VDM++, Section 3.2 describes how various forms of aggregation can be formally defined, Section 3.3 describes alternative approaches for operation formalisation, and for deferring the localisation of methods in classes. Section 3.4 describes the formalisation of dynamic models in the two languages, Section 3.5 considers translation from the notations of the Booch method, Section 3.6 describes general principles for creation of formal classes, and Section 3.7 describes the role of animation in specification enhancement.


Formal Specification Object Model Source State Mutual Exclusion Requirement Elicitation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London Limited 1995

Authors and Affiliations

  • Kevin Lano
    • 1
  1. 1.Department of ComputingImperial College of Science, Technology and MedicineLondonUK

Personalised recommendations