Faculty of Information Technology
Refer to the specific census and withdrawal dates for the semester(s) in which this unit is offered.
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:
Examination (2 hours): 50%; In-semester assessment: 50%
Minimum total expected workload equals 12 hours per week comprising:
(a.) Contact hours for on-campus students:
(b.) Additional requirements (all students):
See also Unit timetable information
Dr Yuan-Fang Li
FIT2004 and one of MAT1830, MTH1112 or MAT1077
A knowledge of set theory, predicate logic, graph, automata and declarative programming is assumed, together with some experience in dealing with the first two.