Module Identifier SE33010  
Module Title FORMAL METHODS IN SOFTWARE ENGINEERING  
Academic Year 2005/2006  
Co-ordinator Dr Frederick W Long  
Semester Semester 2  
Other staff Dr Frederick W Long, Dr Lynda A Thomas  
Pre-Requisite CS21120 , CS22120  
Course delivery Lecture    
  Other   Workshops: 4 x 1 hour  
Assessment
Assessment TypeAssessment Length/DetailsProportion
Semester Exam2 Hours Written Examination  80%
Semester Assessment Two pieces of assessed coursework  20%
Supplementary Exam2 Hours Written Examination  100%
Further details http://www.aber.ac.uk/compsci/ModuleInfo/SE33010  

Learning outcomes

On successful completion of this module students should be able to:
1. 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;

2. be able to differentiate between algebraic and operational approaches to formal specification, and be aware of some of the methods used in industry

3. explain the nature of formal proof in the prepositional and predicate logics and have a critical appreciation of the need for the 3 valued logic of partial functions

4. be able to develop a software design using VDM;

5. have a critical appreciation of the deficiencies of VDM and the attempts to overcome these in some other formal specification methods;

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.

Content

1. The Traditional Approach to Specification - 1 Lecture

Problems of incompleteness, inconsistency and ambiguity. Practical problems (volume of paperwork, etc.).

2. Formal Specifications - 5 Lectures, 1 workshop

The advantages and disadvantages of formal specification. Algebraic and operational specifications. Formal logic and formal proof used in specification.

3. VDM as a Specification Language - 4 Lectures, 1 workshop

Introduction and history. The VDM specification language. Data types in VDM. An example specification.

4. The Logic of Partial Functions - 1 Lecture

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 - 4 Lectures

Stages and processes in the development of a software design using VDM. Data reification and operation decomposition.

6. Correctness Proofs - 4 Lectures, 1 workshop

Programming proof rules and their application in the specification of computer systems.

7. Outstanding Problems and Other Methods - 3 Lectures

Formal specification of systems with concurrency. Modularisation of formal specifications. Safety and reliability issues. Other specification languages, Z and SPARK.

Module Skills

Problem_solving The mathematical logic included in this module involves some problem solving, and this is assessed in the written examination.  
Research skills The assessed coursework requires students to research issues associated with the module.  
Communication The assessed coursework requires students to communicate their research findings.  
Improving own Learning and Performance The assessed coursework requires students to develop their understanding of issues associated with the module.  
Team work None  
Information Technology This is a Software Engineering module!  
Application of Number No! The mathematics involved here is far more abstract and advanced than the mere ability to count!  
Personal Development and Career planning The issues involved in this module could have a significant impact on the career of a Software Engineer.  
Subject Specific Skills The module develops and assesses some advanced issues in Software Engineering.  

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 The Z Notation: A Reference Manual. 2nd. International Series in Computer Science Prentice-Hall
J. Woodcock and M. Loomes (1988) Software Engineering Mathematics Pitman
J G P Barnes (2003) High Integrity Software: The SPARK Approach to Safety and Security Addison-Wesley

Notes

This module is at CQFW Level 6