From Analysis to Formal Specification
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 . Chapter 7 will cover the OMT notation in greater depth, and also consider the OOA method . 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.
KeywordsFormal Specification Object Model Source State Mutual Exclusion Requirement Elicitation
Unable to display preview. Download preview PDF.