Module Identifier | SE33010 | ||||||||||||||
Module Title | FORMAL METHODS IN SOFTWARE ENGINEERING | ||||||||||||||
Academic Year | 2006/2007 | ||||||||||||||
Co-ordinator | Dr Frederick W Long | ||||||||||||||
Semester | Semester 2 | ||||||||||||||
Other staff | Dr Lynda A Thomas, Dr Frederick W Long | ||||||||||||||
Pre-Requisite | CS21120 | ||||||||||||||
Course delivery | Lecture | 22 Hours. | |||||||||||||
Other | Workshops: 4 x 1 hour | ||||||||||||||
Assessment |
| ||||||||||||||
Further details | http://www.aber.ac.uk/compsci/ModuleInfo/SE33010 |
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.
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. |
This module is at CQFW Level 6