Skip to main navigationSkip to main content
The University of Southampton

COMP2214 Advanced Software Modelling and Design

Module Overview

This module builds on the Part 1 Software Modelling and Design Course by looking at structured requirements engineering in more detail, by addressing scaling of formal modelling with Event-B through refinement and also looking at verification techniques for models and for programs.

Aims and Objectives

Learning Outcomes

Knowledge and Understanding

Having successfully completed this module, you will be able to demonstrate knowledge and understanding of:

  • Structured requirements analysis methods
  • Structured design methods and design patterns
  • The role of formal methods and their relevance to software engineering
  • The role of model refinement in Event-B
  • The role of verification in formal development
  • The relationship between specifications and implementations
Subject Specific Intellectual and Research Skills

Having successfully completed this module you will be able to:

  • Derive software requirements in a systematic way
  • Applying structured design methods to software development
  • Construct a formal specification from a set of English language requirements
  • Apply refinement to Event-B models
  • Apply verification techniques to Event-B models
Subject Specific Practical Skills

Having successfully completed this module you will be able to:

  • Document and typeset a specification using a standard word processor
  • Use a UML drawing tool
  • Analyse an Event-B specification using Rodin


- Goal-structured requirements analysis - Design goals - System/service decomposition - Component models - Formal methods in industry - Modelling in Event-B - Proof in Event-B - Model checking in Event-B - Model structuring and refinement - Model decomposition - Reasoning about programs - Preconditions, postconditions, loop invariants, loop variants

Learning and Teaching

Completion of assessment task34
Wider reading or practice106
Total study time150

Resources & Reading list

Bruegge, B. and Dutoit, A.H. (2010). Object-oriented software engineering : using UML, Patterns, and Java. 

Abrial JR (2010). Modelling in Event-B. 

Backhouse R (2003). Program Construction: Calculating Implementations from Specifications. 



MethodPercentage contribution
Continuous Assessment 25%
Final Assessment  75%


MethodPercentage contribution
Set Task 100%


MethodPercentage contribution
Set Task 100%

Repeat Information

Repeat type: Internal & External

Linked modules

Pre-requisites: COMP1202 AND COMP1216

Share this module Share this on Facebook Share this on Twitter Share this on Weibo
Privacy Settings