module specification

The module introduces a model based formal specification language that is used to provide the students with knowledge and skills to produce formal specifications from informal descriptions.
 

Prerequisite: MA1032N Logic or CC2010N Programming and Data Structures or equivalent
Co-requisite: CC3008N Software Architecture

The principal graduate attributes focused on in the module are ‘Performance in a variety of idioms and contexts’ [A2] and ‘Creative and Ethical’ [A3].
The module aims to introduce a model based formal specification language [A2] and provide students with the knowledge and skills to construct formal specifications from informal descriptions [A2, A3] as well as refine their specifications for implementation [A3].

- Rationale for the use of formal specification [A2].
- In-depth study of a model based formal specification language (e.g. Z) [A2].:
o Representational and procedural abstraction using sets and logic, relations, functions and sequences.
o The schema calculus.
o The mathematical toolkit.
o Extension of the language via generic axiomatic definition.
- Software tools to support specification development [A2]..
- Development of substantial case studies, individually and in groups [A2, A3]..
· Basics on Object-oriented variation of the formal specification language already introduced (e.g. Object Z) [A2].

Students will develop their theoretical understanding from interactive lectures (22 hours). Typically, a new concept will be introduced, then used in developing and discussing many small specification fragments. Such lectures will be concentrated at the beginning of the course. Supervised tutorials (22 hours ) will be used for development of larger specifications, often in groups, which will require the application of more of the taught material. The students will also be required to undertake non-supervised work (106 hours) on individual and group case studies, some of which will be part of the assessment for the module. The implementation of the latter will also be part of the assessment for the co-requisite module CC3008N.

On completing the module the student should be able to (the attributes achieved are in brackets):
LO1 - Understand the advantages of using formal specification [A2]
LO2 - Develop formal specifications from informal problem statements [A2, A3].
LO3 - Understand and critically appraise specifications written by others [A2].
LO4 - Refine specifications through different levels of abstraction [A2, A3].
LO5 - Extend the specification language where necessary for an application [A3].

This module is assessed through a coursework and an examination.

- The coursework assignment is based on a Case Study, consisting of a formal specification produced on the basis of provided informal descriptions of requirements. This part is conducted in a group in order to encourage communication and to guide the students to undertake solving a problem in a guided group structure. Formative feedback is provided throughout the whole of the duration of the coursework.
This assessment component assesses the Learning Outcomes LO3 ,LO4 and LO5.

- The final examination is a summative assessment and examines the students’ knowledge and understanding of formal specification in general as well as ability to develop formal specifications from informal problem statements and understand the meaning of other formal specifications. This component assesses the students in Learning Outcomes LO1, LO2, LO3 and LO4.

Currie, E
The Essence of Z
Prentice Hall Europe.

Lightfoot, D
Formal Specification using Z
Palgrave

Woodcock, J. and Davies, J.
Using Z
Prentice Hall;