Advanced Software Modelling and Design

Learning Outcomes

Subject Specific Intellectual and Research Skills

Having successfully completed this module you will be able to:

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

Knowledge and Understanding

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

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

Subject Specific Practical Skills

Having successfully completed this module you will be able to:

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

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