Your programme is made up of credits, the total differs on programme to programme.
Semester 1 Credit Value: | 10 |
ECTS Credits: | 5.0 |
European Credit Transfer System | |
To train students with practical aspects of formal modelling and verification technology as parts of a well-founded set of tools and techniques within software engineering.
1. Background
2. The nature of software (SW) verification; verification principles (correctness, concurrency, abstraction, refinement, design decisions, documented assumptions, model-based testing)
3. Understanding expertise required and costs involved; identifying the right technique to the task at hand.
4. Modelling and Specification
5. From a requirements document and produce an initial abstract specification of the problem.
6. Elicit properties of interest from these requirements as formal consistency conditions, and make a specification of them that is amenable to analysis and verification.
7. Foundations of formal modelling: propositional and predicate logic, data types and invariants; state-based models; mathematical toolkits.
8. Propose design decisions as improved specifications; designs must be amenable to proof and consistency checking of desired properties;
9. Possibly propose code-level contracts from formal design.
10. Verification & Validation
11. Understand verification support systems able to discharge formal consistency conditions from modelling activities
12. Understand what it means for one specification to be a design refinement of another by establishing a link from the requirements to code-contracts
13. Study alternative (to formal) techniques aiming at understanding the costs and conditions under which to undertake a formal or rigorous development process.
14. Understand the importance of automated proof support and proof engineering (i.e. the process of mechanising a complex model)
15. Metrics for complexity, reliability, expertise, time costs
Category | Activity | Number | Length | Student Hours | Comment |
---|---|---|---|---|---|
Guided Independent Study | Assessment preparation and completion | 20 | 1:00 | 20:00 | Lecture follow-up |
Structured Guided Learning | Lecture materials | 10 | 1:00 | 10:00 | Recorded Lectures |
Scheduled Learning And Teaching Activities | Small group teaching | 8 | 1:00 | 8:00 | Practicals as Present in Person OR Online scheduled |
Scheduled Learning And Teaching Activities | Small group teaching | 12 | 1:00 | 12:00 | Synchronous online interactive session |
Guided Independent Study | Project work | 30 | 1:00 | 30:00 | Coursework |
Guided Independent Study | Independent study | 20 | 1:00 | 20:00 | Background reading and tool usage practicing |
Total | 100:00 |
Lectures provide the knowledge. Practicals to provide additional background.
The format of resits will be determined by the Board of Examiners
Description | Semester | When Set | Percentage | Comment |
---|---|---|---|---|
Design/Creative proj | 1 | M | 100 | n/a |
The coursework allows students to reflect upon the practical aspects of formal modelling and verification technology.