units

FIT5138

Faculty of Information Technology

Postgraduate - Unit

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

Refer to the specific census and withdrawal dates for the semester(s) in which this unit is offered, or view unit timetables.

LevelPostgraduate
FacultyFaculty of Information Technology
OfferedNot offered in 2014

Synopsis

This unit covers the core software engineering disciplines concerned with formally modelling software systems using logics and verifying the correctness of such specifications using mechanical/automated proof tools. Topics include mathematical logic, formal specification languages, theorem proving and model checking. It shows how to analyse model complex software systems, how to express properties that the system should adhere to and how to use mechanical/automated proof tools to formally verify such properties.

Outcomes

On successful completion of this unit students should be able to:

  • articulate the role of formal logic and verification methods in the system development life cycle;
  • categorise major techniques and approaches to software verification: theorem proving, model checking and model-based testing;
  • develop software specifications and express desirable properties using a formal language such as the Event-B notation and LTL;
  • install and use a theorem prover such as Rodin on a *nix/Mac OS X/Windows platform to verify the correctness of properties;
  • install and use a LTL model checking system to verify the correctness of a system's temporal properties.

Assessment

Examination (3 hours): 60%, In-semester assessment: 40%

Chief examiner(s)

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

(b.) Additional requirements (all students):

  • A minimum of 8 hours independent study per week for completing tutorial and project work, private study and revision.

Prerequisites