CS33310 - FORMAL METHODS IN SOFTWARE ENGINEERING

Module Identifier	CS33310
Module Title	FORMAL METHODS IN SOFTWARE ENGINEERING
Academic Year	2002/2003
Co-ordinator	Dr Mark B Ratcliffe
Semester	Semester 2
Other staff	Dr Frederick W Long, Dr Ross D King
Pre-Requisite	CS21120 , CS22120
Course delivery	Lecture	22 lectures
	Other	Workshop. Up to 4
Assessment	Semester Exam	2 Hours A1	80%
	Semester Assessment	A2 Course Work: Two pieces	20%
	Supplementary Exam	Will take the same form, under the terms of the Department's policy
Further details	http://www.aber.ac.uk/compsci/ModuleInfo/CS33310

Learning outcomes

On successful completion of this module students should:

have a critical appreciation of the problems of incompleteness, inconsistency and ambiguity arising from traditional methods of software specification, and of how formal methods overcome these problems (A1);
be familiar with the different approaches to formal specification and of some of the formal methods used in industry (A1, A2);
be familiar with the nature of formal proof in the propositional and predicate logics and have a critical appreciation of the need for the three valued logic of partial functions (A1);
be able to develop a software design using VDM (A1);
have a critical appreciation of the deficiencies of VDM and the attempts to overcome these in some other formal specification methods (A1, A2);
be familiar with some other logics, and their application to solving problems in Computer Science (A1).

Brief description

The module introduces students to the use of mathematically formal methods for the specification of software. As background to the formal methods in software engineering, students are introduced to formal logic and some of its other applications in Computer Science.

Aims

This module aims to introduce students to the use of formal methods in software specification. It develops the underlying ideas by presenting mathematical logic in a formal way, illustrating a number of different logics, and by showing some of the other applications of logic in Computer Science. The practical elements of the module aim to consolidate and extend the material presented in the lectures.

Content

1. The Traditional Approach to Specification - 1 Lecture
Problems of incompleteness, inconsistency and ambiguity. Practical problems (volume of paperwork, etc.).

2. Formal Specifications - 1 Lecture
The advantages and disadvantages of formal specification. Algebraic and operational specifications.

3. VDM as a Specification Language - 4 Lectures
Introduction and history. The VDM specification language. Data types in VDM. Proof using the data types. An example specification.

4. The Logic of Partial Functions - 2 Lectures
Proof in the three valued logic of partial functions. Differences from the traditional two valued logic. Applications to formal methods, in particular VDM.

5. VDM as a Formal Development Method - 3 Lectures
Stages and processes in the development of a software design using VDM. Data reification and operation decomposition.

6. Correctness Proofs - 3 Lectures
Programming proof rules and their application in the specification of computer systems.

7. Outstanding Problems and Other Methods - 2 Lectures
Formal specification of systems with concurrency. Modularisation of formal specifications. Safety and reliability issues. Other specification languages, Z and GYPSY (briefly). ANNA and SPARK.

8. Temporal Logic - 2 Lectures
Specification of time dependent systems. The operators always, sometimes, next and until. Extension of VDM to include temporal logic.

9. Logic Applications in Computing - 4 Lectures
Resolution theorem proving. Logic programming and Prolog. Multi-valued logics, Fuzzy logic, and reasoning with uncertainty.

Reading Lists

Books
** Recommended Text
R.D. Dowsing, V.J. Rayward-Smith, and C.D. Walter. (1986) A First Course in Formal Logic and its Application in Computer Science. Computer Science Texts, Blackwell Scientific Publications
C.B. Jones. (1990) Systematic Software Development Using VDM. 2nd. International Series in Computer Science. Prentice-Hall
** Consult For Futher Information
J.M. Spivey. (1992) The Z Notation: A Reference Manual. 2nd. International Series in Computer Science. Prentice-Hall
D. Bjorner, C.A.R Hoare, and H. Langmaack, editors. (1990) VDM '90: VDM and Z - Formal Methods in Software Development [volume 428 of LNCS]. Springer-Verlag
J G P Barnes. (1997) High Integrity Ada: The SPARK Approach. Addison-Wesley
J. Woodcock and M. Loomes. (1988) Software Engineering Mathematics. Pitman