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
Knowledge and Understanding
Having successfully completed this module, you will be able to demonstrate knowledge and understanding of:
- Structured requirements analysis methods
- The role of verification in formal development
- The relationship between specifications and implementations
- 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
Subject Specific Intellectual and Research Skills
Having successfully completed this module you will be able to:
- Applying structured design methods to software development
- Apply verification techniques to Event-B models
- Construct a formal specification from a set of English language requirements
- Apply refinement to Event-B models
- Derive software requirements in a systematic way
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
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
Type | Hours |
---|---|
Wider reading or practice | 106 |
Completion of assessment task | 34 |
Revision | 10 |
Total study time | 150 |
Resources & Reading list
Textbooks
Backhouse R (2003). Program Construction: Calculating Implementations from Specifications. Wiley.
Bruegge, B. and Dutoit, A.H. (2010). Object-oriented software engineering : using UML, Patterns, and Java. Pearson.
Abrial JR (2010). Modelling in Event-B. CUP.
Assessment
Summative
This is how we’ll formally assess what you have learned in this module.
Method | Percentage contribution |
---|---|
Final Assessment | 75% |
Continuous Assessment | 25% |
Referral
This is how we’ll assess you if you don’t meet the criteria to pass this module.
Method | Percentage contribution |
---|---|
Set Task | 100% |
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.
Method | Percentage contribution |
---|---|
Set Task | 100% |
Repeat Information
Repeat type: Internal & External