Module Identifier 
SE33010 
Module Title 
FORMAL METHODS IN SOFTWARE ENGINEERING 
Academic Year 
2003/2004 
Coordinator 
Dr Mark B Ratcliffe 
Semester 
Semester 1 
Other staff 
Dr Frederick W Long 
PreRequisite 
CS21120 , CS22120 
Course delivery 
Lecture  22 Hours 

Other  Workshops: 4 x 1 hour 
Assessment 
Assessment Type  Assessment Length/Details  Proportion 
Semester Exam  2 Hours Written Examination  80% 
Semester Assessment  Two pieces of assessed coursework  20% 
Supplementary Exam  2 Hours Written Examination  100% 

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  3 Lecture, 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.
8. Temporal Logic  2 Lectures
Specification of time dependent systems. The operators always, sometimes, next and until. Extension of VDM to include temporal logic.
Reading Lists
Books
** Recommended Text
R.D. Dowsing, V.J. RaywardSmith, 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
PrenticeHall
** Consult For Futher Information
J. Woodcock and M. Loomes (1988) Software Engineering Mathematics
Pitman
J.M. Spivey The Z Notation: A Reference Manual. 2nd. International Series in Computer Science
PrenticeHall
J G P Barnes (1997) High Integrity Ada: The SPARK Approach
AddisonWesley
Notes
This module is at CQFW Level 6