Module Identifier | CS33310 | ||

Module Title | FORMAL METHODS IN SOFTWARE ENGINEERING | ||

Academic Year | 2000/2001 | ||

Co-ordinator | Dr Mark Ratcliffe | ||

Semester | Semester 2 | ||

Pre-Requisite | CS21020 or CS22120, CS22120 | ||

Course delivery | Lecture | 22 lectures | |

Seminars / Tutorials | (Up to) 4 workshops | ||

Assessment | Exam | 2 Hours | 80% |

Course work | Two pieces | 20% | |

Supplementary examination | Will take the same form, under the terms of the Department's policy | |

**General 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.

**Learning outcomes**

On successful completion of this course students should understand:

- the problems of incompleteness, inconsistency and ambiguity arising from traditional methods of software specification;

- the different approaches to formal specification;

- the nature of formal proof in the propositional and predicate logics;

- the stages and processes involved in the development of a software design using VDM;

- the need for the three valued logic of partial functions and how to carry out formal proof in that logic;

- the ideas behind correctness proofs of computer code and how to carry out such proofs themselves;

- how proof is applied to the data types of VDM;

- the deficiencies of VDM and the attempts to overcome these in some other formal specification methods;

- temporal logic and its application to the specification of concurrent systems;

- the applications of logic in resolution theorem proving, logic programming, expert systems, and fuzzy systems.

**Syllabus**

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**
**** Should Be Purchased**

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 G P Barnes. (1997)
*High Integrity Ada: The SPARK Approach*. Addison-Wesley

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.M. Spivey. (1992)
*The Z Notation: A Reference Manual*. 2nd. International Series in Computer Science. Prentice-Hall

J. Woodcock and M. Loomes. (1988)
*Software Engineering Mathematics*. Pitman