The University of Southampton
Courses

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

Module Aims

This modules aims: - To encourage proficient use of structured requirements analysis methods - To encourage proficient use of structured design methods and design patterns - To increase understanding of the relationship between formal modelling and software engineering - To encourage proficient use of refinement and verification in Event-B - To increase awareness of the relationship between formal modelling and correct software implementations - To raise awareness of a range of formal approaches to software verification

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 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
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

Syllabus

- 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

TypeHours
Revision10
Wider reading or practice106
Completion of assessment task34
Total study time150

Resources & Reading list

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

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

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

Assessment

Summative

MethodPercentage contribution
Coursework 25%
Exam  (2 hours) 75%

Referral

MethodPercentage contribution
Exam 100%

Repeat Information

Repeat type: Internal & External

Linked modules

Pre-requisites: COMP1202 (Programming I) AND COMP1216 (Software Modelling And Design)

Share this module Facebook Google+ Twitter Weibo

We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.

×