units

FIT3013

Faculty of Information Technology

18 September 2017 22 December 2024

print version

This unit entry is for students who completed this unit in 2016 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.

Monash University

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.

Faculty

Information Technology

Offered

Clayton

  • Second semester 2016 (Day)

Synopsis

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.

Outcomes

At the completion of this unit, students should be able to:

  1. articulate the role and importance of formal modelling and verification;
  2. develop Event-B specifications;
  3. apply Rodin to analyse an Event-B specification and verify proof obligations;
  4. distinguish and evaluate the trade-offs in system modelling using Event-B and temporal logics;
  5. develop basic specifications and formulate properties in temporal logics;
  6. utilise a model checker to verify such properties.

Assessment

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

Workload requirements

Minimum total expected workload equals 12 hours per week comprising:

(a.) Contact hours for on-campus students:

  • Two hours of lectures
  • One 2-hour tutorial/lab

(b.) 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

Chief examiner(s)

Dr Yuan-Fang Li

Prerequisites

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.

Prohibitions

CSE4213

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

http://www.infotech.monash.edu.au/units/