Advanced Software Modelling and Design

Learning Outcomes

Subject Specific Practical Skills

Having successfully completed this module you will be able to:

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

Subject Specific Intellectual and Research Skills

Having successfully completed this module you will be able to:

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

Knowledge and Understanding

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

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

• 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

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.