|Module Title||FORMAL METHODS IN SOFTWARE ENGINEERING|
|Co-ordinator||Dr Frederick W Long|
|Other staff||Dr Lynda A Thomas, Mr David J Smith, Dr Frederick W Long|
|Course delivery||Lecture||22 Hours.|
|Other||Workshops: 4 x 1 hour|
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.|
|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