6 points, SCA Band 2, 0.125 EFTSL
Undergraduate - Unit
Refer to the specific census and withdrawal dates for the semester(s) in which this unit is offered.
- Second semester 2017 (Day)
Review of set theory, the predicate calculus, relations, relational algebra and formal specification concepts; algebraic and model based specifications; the role of formal specifications in software engineering. The Event-B notation, the role of proof obligations and refinement, the LTL and CTL temporal logics, the model checking approach and techniques.
At the completion of this unit, students should be able to:
- articulate the role and importance of formal modelling and verification;
- develop Event-B specifications;
- apply Rodin to analyse an Event-B specification and verify proof obligations;
- distinguish and evaluate the trade-offs in system modelling using Event-B and temporal logics;
- develop basic specifications and formulate properties in temporal logics;
- utilise a model checker to verify such properties.
Examination (2 hours): 50%; In-semester assessment: 50%
Minimum total expected workload equals 12 hours per week comprising:
- Contact hours for on-campus students:
- Two hours of lectures
- One 2-hour tutorial/lab
- Additional requirements (all students):
- A minimum of 8 hours independent study per week for completing lab and project work, private study and revision.
See also Unit timetable information
This unit applies to the following area(s) of study
A knowledge of set theory, predicate logic, graph, automata and declarative programming is assumed, together with some experience in dealing with the first two.