Hello, if you have any need, please feel free to consult us, this is my wechat: wx91due

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.

Linked modules

Pre-requisites: COMP1202 AND COMP1216

Aims and Objectives

Learning Outcomes

Subject Specific Practical Skills

Having successfully completed this module you will be able to:

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

Knowledge and Understanding

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

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

Subject Specific Intellectual and Research Skills

Having successfully completed this module you will be able to:

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

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

Resources & Reading list

Textbooks

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

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

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

Assessment

Summative

This is how we’ll formally assess what you have learned in this module.

Referral

This is how we’ll assess you if you don’t meet the criteria to pass this module.

Repeat

An internal repeat is where you take all of your modules again, including any you passed. An external repeat is where you only re-take the modules you failed.

Repeat Information

Repeat type: Internal & External