Module Title:   Formal Methods

Module Credit:   20

Module Code:   CM-0332D

Academic Year:   2015/6

Teaching Period:   Semester 1

Module Occurrence:   A

Module Level:   FHEQ Level 6

Module Type:   Standard module

Provider:   Computer Science

Related Department/Subject Area:   School of Electrical Engineering & Computer Science

Principal Co-ordinator:   Dr S Konur

Additional Tutor(s):   Prof M Gheorghe

Prerequisite(s):   CM-0111L

Corequisite(s):   None

Aims:
To build upon the knowledge and skills gained in CM-0111L by examining the role of formal methods in software engineering and providing a detailed study of a widely-used formal specification notation.

Learning Teaching & Assessment Strategy:
The delivery of the module will consist of directed reading, lectures to expand upon key points in the reading, and tutorials where practical problems are introduced and solved. The coursework assesses students understanding of the technical skills required by the module, while the examination tests their ability to apply those skills.

Lectures:   24.00          Directed Study:   161.00           
Seminars/Tutorials:   12.00          Other:   0.00           
Laboratory/Practical:   0.00          Formal Exams:   3.00          Total:   200.00

On successful completion of this module you will be able to...

understand comprehensively the role of formal methods in software development.

On successful completion of this module you will be able to...

apply a formal notation for specifying the functional requirements for software systems.

On successful completion of this module you will be able to...

think abstractly about system requirements.

  Coursework   20%
 
  Individual coursework, consisting of undertaking a specification case study.
  Examination - closed book 3.00 80%
 
  Exam
  Examination - closed book 3.00 100%
 
  Supplementary exam.

Outline Syllabus:
1. Basic principles of classical logic.
2. Formal specification languages and their use in program requirements.
3. Formal verification techniques (e.g. model checking) for analysis of software systems.

Version No:  4