Faculty of Information Technology

Monash University

Undergraduate - Unit

This unit entry is for students who completed this unit in 2013 only. For students planning to study the unit, please refer to the unit indexes in the the current edition of the Handbook. If you have any queries contact the managing faculty for your course or area of study.

print version

6 points, SCA Band 2, 0.125 EFTSL

To find units available for enrolment in the current year, you must make sure you use the indexes and browse unit tool in the current edition of the Handbook.

FacultyFaculty of Information Technology
OfferedClayton Second semester 2013 (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 will 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 LTL;
  • Develop basic LTL specifications and formulate LTL properties;
  • Apply a model check to verify LTL properties.


Examination (2 hours): 50%; In-semester assessment: 50%

Chief examiner(s)

Contact hours

2 hrs lectures/wk, 1 hr tutorial/wk

3 x 2 hrs laboratories during the semester for hands-on practice with Rodin and Event-B.

This unit applies to the following area(s) of study


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.



Additional information on this unit is available from the faculty at: